{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
1 is non empty set
{{},1} is non empty set
K47() is set
bool K47() is non empty set
{{}} is functional non empty set
F1() is set
A is Relation-like Function-like set
proj1 A is set
B is Relation-like Function-like set
A . B is set
F2(B) is set
~ {} is Relation-like Function-like set
[:{},{}:] is Relation-like set
proj1 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
proj1 (~ {}) is set
proj1 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
proj2 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
A is set
B is set
[:B,A:] is Relation-like set
[:A,B:] is Relation-like set
proj1 [:B,A:] is set
proj2 [:A,B:] is set
the Element of A is Element of A
f is set
[f, the Element of A] is V22() set
{f, the Element of A} is non empty set
{f} is non empty set
{{f, the Element of A},{f}} is non empty set
a is set
[f,a] is V22() set
{f,a} is non empty set
{{f,a},{f}} is non empty set
f is set
[ the Element of A,f] is V22() set
{ the Element of A,f} is non empty set
{ the Element of A} is non empty set
{{ the Element of A,f},{ the Element of A}} is non empty set
a is set
[a,f] is V22() set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
proj1 [:A,B:] is set
proj2 [:A,B:] is set
C is set
f is set
[C,f] is V22() set
{C,f} is non empty set
{C} is non empty set
{{C,f},{C}} is non empty set
C is set
f is set
[f,C] is V22() set
{f,C} is non empty set
{f} is non empty set
{{f,C},{f}} is non empty set
A is set
proj1 A is set
proj2 A is set
B is set
C is set
[:B,C:] is Relation-like set
proj1 [:B,C:] is set
proj2 [:B,C:] is set
A is set
{A} is non empty set
B is set
[A,B] is V22() set
{A,B} is non empty set
{{A,B},{A}} is non empty set
{[A,B]} is Relation-like Function-like non empty set
proj1 {[A,B]} is non empty set
proj2 {[A,B]} is non empty set
{B} is non empty set
C is set
f is set
[C,f] is V22() set
{C,f} is non empty set
{C} is non empty set
{{C,f},{C}} is non empty set
C is set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
C is set
f is set
[f,C] is V22() set
{f,C} is non empty set
{f} is non empty set
{{f,C},{f}} is non empty set
C is set
[A,C] is V22() set
{A,C} is non empty set
{{A,C},{A}} is non empty set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is set
{A,C} is non empty set
f is set
[C,f] is V22() set
{C,f} is non empty set
{C} is non empty set
{{C,f},{C}} is non empty set
{[A,B],[C,f]} is Relation-like non empty set
proj1 {[A,B],[C,f]} is non empty set
proj2 {[A,B],[C,f]} is non empty set
{B,f} is non empty set
{[A,B]} is Relation-like Function-like non empty set
proj2 {[A,B]} is non empty set
{B} is non empty set
{[C,f]} is Relation-like Function-like non empty set
proj2 {[C,f]} is non empty set
{f} is non empty set
{[A,B]} \/ {[C,f]} is Relation-like non empty set
proj1 {[A,B]} is non empty set
proj1 {[C,f]} is non empty set
(proj1 {[A,B]}) \/ (proj1 {[C,f]}) is non empty set
(proj2 {[A,B]}) \/ (proj2 {[C,f]}) is non empty set
A is set
proj1 A is set
proj2 A is set
the Element of proj2 A is Element of proj2 A
the Element of proj1 A is Element of proj1 A
f is set
[ the Element of proj1 A,f] is V22() set
{ the Element of proj1 A,f} is non empty set
{ the Element of proj1 A} is non empty set
{{ the Element of proj1 A,f},{ the Element of proj1 A}} is non empty set
C is set
[C, the Element of proj2 A] is V22() set
{C, the Element of proj2 A} is non empty set
{C} is non empty set
{{C, the Element of proj2 A},{C}} is non empty set
A is set
proj1 A is set
proj2 A is set
B is set
C is set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
A is set
proj1 A is set
proj2 A is set
B is set
C is set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
A is Relation-like Function-like set
proj1 A is set
proj1 (proj1 A) is set
~ A is Relation-like Function-like set
proj1 (~ A) is set
proj2 (proj1 (~ A)) is set
proj2 (proj1 A) is set
proj1 (proj1 (~ A)) is set
B is set
C is set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
B is set
C is set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
B is set
C is set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
B is set
C is set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
A is Relation-like set
proj1 A is set
B is Relation-like set
proj2 B is set
A is Relation-like Function-like set
proj1 A is set
proj1 (proj1 A) is set
proj2 (proj1 A) is set
B is set
{B} is non empty set
[:{B},(proj2 (proj1 A)):] is Relation-like set
(proj1 A) /\ [:{B},(proj2 (proj1 A)):] is Relation-like set
proj2 ((proj1 A) /\ [:{B},(proj2 (proj1 A)):]) is set
C is set
f is set
a is Relation-like Function-like set
proj1 a is set
b is Relation-like Function-like set
proj1 b is set
t is set
a . t is set
A . (B,t) is set
[B,t] is V22() set
{B,t} is non empty set
{{B,t},{B}} is non empty set
A . [B,t] is set
b . t is set
B is set
{B} is non empty set
[:{B},(proj2 (proj1 A)):] is Relation-like set
(proj1 A) /\ [:{B},(proj2 (proj1 A)):] is Relation-like set
proj2 ((proj1 A) /\ [:{B},(proj2 (proj1 A)):]) is set
C is Relation-like Function-like set
proj1 C is set
f is set
a is set
C . a is set
A . (B,a) is set
[B,a] is V22() set
{B,a} is non empty set
{{B,a},{B}} is non empty set
A . [B,a] is set
B is Relation-like Function-like set
proj1 B is set
B is Relation-like Function-like set
proj1 B is set
C is Relation-like Function-like set
proj1 C is set
f is set
B . f is set
{f} is non empty set
[:{f},(proj2 (proj1 A)):] is Relation-like set
(proj1 A) /\ [:{f},(proj2 (proj1 A)):] is Relation-like set
proj2 ((proj1 A) /\ [:{f},(proj2 (proj1 A)):]) is set
a is Relation-like Function-like set
proj1 a is set
C . f is set
b is Relation-like Function-like set
proj1 b is set
t is set
a . t is set
A . (f,t) is set
[f,t] is V22() set
{f,t} is non empty set
{{f,t},{f}} is non empty set
A . [f,t] is set
b . t is set
B is set
A .: B is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
union (proj2 C) is set
[:B,(union (proj2 C)):] is Relation-like set
f is set
a is set
a `1 is set
A . (a `1) is set
a `2 is set
b is Relation-like Function-like set
b . (a `2) is set
a is set
g1 is Relation-like Function-like set
a `1 is set
A . (a `1) is set
b is set
a `2 is set
g1 . (a `2) is set
z is Relation-like Function-like set
t is set
z . (a `2) is set
a is Relation-like Function-like set
proj1 a is set
b is set
b `1 is set
t is set
A . t is set
g1 is Relation-like Function-like set
proj1 g1 is set
b `2 is set
[t,(b `2)] is V22() set
{t,(b `2)} is non empty set
{t} is non empty set
{{t,(b `2)},{t}} is non empty set
t is set
z is set
[t,z] is V22() set
{t,z} is non empty set
{t} is non empty set
{{t,z},{t}} is non empty set
g1 is Relation-like Function-like set
A . t is set
proj1 g1 is set
C . g1 is set
b `1 is set
A . (b `1) is set
b `2 is set
g is Relation-like Function-like set
proj1 g is set
b is set
b `1 is set
A . (b `1) is set
a . b is set
b `2 is set
t is Relation-like Function-like set
t . (b `2) is set
g1 is Relation-like Function-like set
g1 . (b `2) is set
B is Relation-like Function-like set
proj1 B is set
C is Relation-like Function-like set
proj1 C is set
f is set
a is set
t is set
[a,t] is V22() set
{a,t} is non empty set
{a} is non empty set
{{a,t},{a}} is non empty set
b is Relation-like Function-like set
A . a is set
proj1 b is set
f `1 is set
f `2 is set
B . f is set
b . t is set
C . f is set
A is Relation-like Function-like set
~ A is Relation-like Function-like set
((~ A)) is Relation-like Function-like set
(A) is Relation-like Function-like set
~ (A) is Relation-like Function-like set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
proj1 (C) is set
(C) . A is set
proj1 (proj1 C) is set
proj2 (proj1 C) is set
[:{A},(proj2 (proj1 C)):] is Relation-like set
(proj1 C) /\ [:{A},(proj2 (proj1 C)):] is Relation-like set
proj2 ((proj1 C) /\ [:{A},(proj2 (proj1 C)):]) is set
f is Relation-like Function-like set
proj1 f is set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
(C) . A is set
C . (A,B) is set
C . [A,B] is set
f is Relation-like Function-like set
proj1 f is set
f . B is set
proj1 (proj1 C) is set
proj2 (proj1 C) is set
[:{A},(proj2 (proj1 C)):] is Relation-like set
(proj1 C) /\ [:{A},(proj2 (proj1 C)):] is Relation-like set
proj2 ((proj1 C) /\ [:{A},(proj2 (proj1 C)):]) is set
a is Relation-like Function-like set
proj1 a is set
a is Relation-like Function-like set
proj1 a is set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
proj1 (C) is set
(C) . B is set
[B,A] is V22() set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
proj1 (~ C) is set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
(C) . B is set
C . (A,B) is set
C . [A,B] is set
f is Relation-like Function-like set
proj1 f is set
f . A is set
[B,A] is V22() set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
proj1 (~ C) is set
(~ C) . (B,A) is set
(~ C) . [B,A] is set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
~ A is Relation-like Function-like set
((~ A)) is Relation-like Function-like set
proj1 (A) is set
proj1 A is set
proj2 (proj1 A) is set
proj1 ((~ A)) is set
proj1 (~ A) is set
proj1 (proj1 (~ A)) is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
proj1 (C) is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
proj1 (C) is set
proj1 (proj1 C) is set
proj1 (~ C) is set
proj1 (proj1 (~ C)) is set
[:B,A:] is Relation-like set
proj1 [:B,A:] is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
proj1 (C) is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
proj1 (C) is set
proj1 (proj1 C) is set
proj1 (~ C) is set
proj1 (proj1 (~ C)) is set
[:B,A:] is Relation-like set
A is set
B is set
Funcs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
proj1 (C) is set
proj1 C is set
[:(proj1 C),A:] is Relation-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
proj1 (C) is set
[:A,(proj1 C):] is Relation-like set
f is set
f `1 is set
C . (f `1) is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
f `2 is set
[(f `1),(f `2)] is V22() set
{(f `1),(f `2)} is non empty set
{(f `1)} is non empty set
{{(f `1),(f `2)},{(f `1)}} is non empty set
a is set
t is set
[a,t] is V22() set
{a,t} is non empty set
{a} is non empty set
{{a,t},{a}} is non empty set
b is Relation-like Function-like set
C . a is set
proj1 b is set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
f is set
a is set
b is set
g1 is set
[b,g1] is V22() set
{b,g1} is non empty set
{b} is non empty set
{{b,g1},{b}} is non empty set
t is Relation-like Function-like set
C . b is set
proj1 t is set
A is Relation-like Function-like set
proj1 A is set
(A) is Relation-like Function-like set
(A) is Relation-like Function-like set
~ A is Relation-like Function-like set
((~ A)) is Relation-like Function-like set
proj1 (proj1 A) is set
proj1 (A) is set
B is set
C is set
[B,C] is V22() set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
proj1 (~ A) is set
[C,B] is V22() set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
proj1 (proj1 (~ A)) is set
proj1 ((~ A)) is set
A is Relation-like Function-like set
proj1 A is set
(A) is Relation-like Function-like set
(A) is Relation-like Function-like set
~ (A) is Relation-like Function-like set
proj1 (A) is set
the Element of proj1 (A) is Element of proj1 (A)
C is set
a is set
[C,a] is V22() set
{C,a} is non empty set
{C} is non empty set
{{C,a},{C}} is non empty set
f is Relation-like Function-like set
A . C is set
proj1 f is set
A is set
B is set
[:A,B:] is Relation-like set
C is set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
(f) . C is set
proj2 f is set
{C} is non empty set
[:{C},B:] is Relation-like set
[:{C},B:] /\ (proj1 f) is Relation-like set
proj1 (proj1 f) is set
proj2 (proj1 f) is set
[:{C},(proj2 (proj1 f)):] is Relation-like set
(proj1 f) /\ [:{C},(proj2 (proj1 f)):] is Relation-like set
proj2 ((proj1 f) /\ [:{C},(proj2 (proj1 f)):]) is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
proj2 [:{C},B:] is set
b is set
t is set
a . t is set
[C,t] is V22() set
{C,t} is non empty set
{{C,t},{C}} is non empty set
f . (C,t) is set
f . [C,t] is set
b is set
a . b is set
f . (C,b) is set
[C,b] is V22() set
{C,b} is non empty set
{{C,b},{C}} is non empty set
f . [C,b] is set
A is set
B is Relation-like Function-like set
(B) is Relation-like Function-like set
proj1 (B) is set
(B) . A is set
proj1 B is set
proj1 (proj1 B) is set
{A} is non empty set
proj2 (proj1 B) is set
[:{A},(proj2 (proj1 B)):] is Relation-like set
(proj1 B) /\ [:{A},(proj2 (proj1 B)):] is Relation-like set
proj2 ((proj1 B) /\ [:{A},(proj2 (proj1 B)):]) is set
C is Relation-like Function-like set
proj1 C is set
A is set
{A} is non empty set
B is Relation-like Function-like set
(B) is Relation-like Function-like set
proj1 (B) is set
(B) . A is set
proj1 B is set
proj2 (proj1 B) is set
[:{A},(proj2 (proj1 B)):] is Relation-like set
(proj1 B) /\ [:{A},(proj2 (proj1 B)):] is Relation-like set
proj2 ((proj1 B) /\ [:{A},(proj2 (proj1 B)):]) is set
proj2 B is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
proj1 (proj1 B) is set
f is Relation-like Function-like set
proj1 f is set
a is set
b is set
C . b is set
t is set
[t,b] is V22() set
{t,b} is non empty set
{t} is non empty set
{{t,b},{t}} is non empty set
[A,b] is V22() set
{A,b} is non empty set
{{A,b},{A}} is non empty set
f . b is set
B . (A,b) is set
B . [A,b] is set
a is set
C . a is set
B . (A,a) is set
[A,a] is V22() set
{A,a} is non empty set
{{A,a},{A}} is non empty set
B . [A,a] is set
b is set
[b,a] is V22() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
C is set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
~ f is Relation-like Function-like set
((~ f)) is Relation-like Function-like set
(f) . C is set
proj2 f is set
proj1 (~ f) is set
[:B,A:] is Relation-like set
((~ f)) . C is set
proj2 (~ f) is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
b is set
a . b is set
f . (b,C) is set
[b,C] is V22() set
{b,C} is non empty set
{b} is non empty set
{{b,C},{b}} is non empty set
f . [b,C] is set
(~ f) . (C,b) is set
[C,b] is V22() set
{C,b} is non empty set
{C} is non empty set
{{C,b},{C}} is non empty set
(~ f) . [C,b] is set
A is set
B is Relation-like Function-like set
(B) is Relation-like Function-like set
~ B is Relation-like Function-like set
((~ B)) is Relation-like Function-like set
proj1 (B) is set
(B) . A is set
A is set
{A} is non empty set
B is Relation-like Function-like set
(B) is Relation-like Function-like set
~ B is Relation-like Function-like set
((~ B)) is Relation-like Function-like set
proj1 (B) is set
(B) . A is set
proj1 B is set
proj1 (proj1 B) is set
[:(proj1 (proj1 B)),{A}:] is Relation-like set
(proj1 B) /\ [:(proj1 (proj1 B)),{A}:] is Relation-like set
proj1 ((proj1 B) /\ [:(proj1 (proj1 B)),{A}:]) is set
proj2 B is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
proj2 (~ B) is set
proj1 (~ B) is set
proj2 (proj1 (~ B)) is set
[:{A},(proj2 (proj1 (~ B))):] is Relation-like set
(proj1 (~ B)) /\ [:{A},(proj2 (proj1 (~ B))):] is Relation-like set
proj2 ((proj1 (~ B)) /\ [:{A},(proj2 (proj1 (~ B))):]) is set
[:{A},(proj1 (proj1 B)):] is Relation-like set
(proj1 (~ B)) /\ [:{A},(proj1 (proj1 B)):] is Relation-like set
proj2 ((proj1 (~ B)) /\ [:{A},(proj1 (proj1 B)):]) is set
f is set
a is set
[a,f] is V22() set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
[f,a] is V22() set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
f is set
a is set
[f,a] is V22() set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
[a,f] is V22() set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
f is set
C . f is set
B . (f,A) is set
[f,A] is V22() set
{f,A} is non empty set
{f} is non empty set
{{f,A},{f}} is non empty set
B . [f,A] is set
a is set
[f,a] is V22() set
{f,a} is non empty set
{{f,a},{f}} is non empty set
[a,f] is V22() set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
(~ B) . (A,f) is set
[A,f] is V22() set
{A,f} is non empty set
{{A,f},{A}} is non empty set
(~ B) . [A,f] is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
proj2 (C) is set
proj2 C is set
Funcs (B,(proj2 C)) is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
proj2 (C) is set
Funcs (A,(proj2 C)) is set
proj1 (C) is set
f is set
a is set
(C) . a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
proj1 (C) is set
f is set
a is set
(C) . a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
[:B,A:] is Relation-like set
proj1 (~ C) is set
proj1 ((~ C)) is set
proj1 (proj1 (~ C)) is set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
proj2 (A) is set
proj1 A is set
proj2 (proj1 A) is set
proj2 A is set
PFuncs ((proj2 (proj1 A)),(proj2 A)) is set
(A) is Relation-like Function-like set
~ A is Relation-like Function-like set
((~ A)) is Relation-like Function-like set
proj2 (A) is set
proj1 (proj1 A) is set
PFuncs ((proj1 (proj1 A)),(proj2 A)) is set
proj2 (~ A) is set
B is set
proj1 (A) is set
C is set
(A) . C is set
{C} is non empty set
[:{C},(proj2 (proj1 A)):] is Relation-like set
(proj1 A) /\ [:{C},(proj2 (proj1 A)):] is Relation-like set
proj2 ((proj1 A) /\ [:{C},(proj2 (proj1 A)):]) is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
B is set
proj1 (A) is set
C is set
(A) . C is set
proj1 ((~ A)) is set
proj1 (~ A) is set
proj1 (proj1 (~ A)) is set
((~ A)) . C is set
{C} is non empty set
proj2 (proj1 (~ A)) is set
[:{C},(proj2 (proj1 (~ A))):] is Relation-like set
(proj1 (~ A)) /\ [:{C},(proj2 (proj1 (~ A))):] is Relation-like set
proj2 ((proj1 (~ A)) /\ [:{C},(proj2 (proj1 (~ A))):]) is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
A is set
B is set
PFuncs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
proj1 (C) is set
proj1 C is set
[:(proj1 C),A:] is Relation-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
proj1 (C) is set
[:A,(proj1 C):] is Relation-like set
f is set
a is set
t is set
[a,t] is V22() set
{a,t} is non empty set
{a} is non empty set
{{a,t},{a}} is non empty set
b is Relation-like Function-like set
C . a is set
proj1 b is set
[:A,B:] is Relation-like set
bool [:A,B:] is non empty set
f is set
b is set
a is set
[b,a] is V22() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
[a,b] is V22() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
A is set
B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
C is Relation-like Function-like set
proj1 C is set
C . A is set
(C) is Relation-like Function-like set
proj1 (C) is set
(C) . (A,B) is set
(C) . [A,B] is set
proj2 (C) is set
f is Relation-like Function-like set
proj1 f is set
f . B is set
[A,B] `1 is set
[A,B] `2 is set
A is set
B is set
[B,A] is V22() set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
C is Relation-like Function-like set
proj1 C is set
C . A is set
(C) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
proj1 (C) is set
(C) . (B,A) is set
(C) . [B,A] is set
proj2 (C) is set
f is Relation-like Function-like set
proj1 f is set
f . B is set
[A,B] is V22() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
proj1 (C) is set
(C) . (A,B) is set
(C) . [A,B] is set
A is set
B is set
PFuncs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
proj2 (C) is set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
proj2 (C) is set
f is set
proj1 (C) is set
a is set
(C) . a is set
proj1 C is set
b is set
g1 is set
[b,g1] is V22() set
{b,g1} is non empty set
{b} is non empty set
{{b,g1},{b}} is non empty set
t is Relation-like Function-like set
C . b is set
proj1 t is set
(C) . (b,g1) is set
(C) . [b,g1] is set
t . g1 is set
proj2 t is set
z is Relation-like Function-like set
proj1 z is set
proj2 z is set
A is set
B is set
Funcs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
proj2 (C) is set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
proj2 (C) is set
PFuncs (A,B) is set
({}) is Relation-like Function-like set
({}) is Relation-like Function-like set
((~ {})) is Relation-like Function-like set
proj1 ({}) is set
proj1 (proj1 {}) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
({}) is Relation-like Function-like set
({}) is Relation-like Function-like set
~ ({}) is Relation-like Function-like set
proj1 ({}) is set
the Element of proj1 ({}) is Element of proj1 ({})
B is set
f is set
[B,f] is V22() set
{B,f} is non empty set
{B} is non empty set
{{B,f},{B}} is non empty set
C is Relation-like Function-like set
{} . B is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
proj1 C is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
a is set
a `1 is set
(C) . (a `1) is set
proj2 C is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
a `2 is set
[(a `1),(a `2)] is V22() set
{(a `1),(a `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
C . ((a `1),(a `2)) is set
C . [(a `1),(a `2)] is set
b . (a `2) is set
(f) . (a `1) is set
proj2 f is set
f . ((a `1),(a `2)) is set
f . [(a `1),(a `2)] is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
C . a is set
f . a is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
~ f is Relation-like Function-like set
((~ f)) is Relation-like Function-like set
proj1 (~ C) is set
[:B,A:] is Relation-like set
proj1 (~ f) is set
~ (~ C) is Relation-like Function-like set
A is set
B is set
Funcs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
f is Relation-like Function-like set
proj2 f is set
(f) is Relation-like Function-like set
proj1 (C) is set
proj1 C is set
[:(proj1 C),A:] is Relation-like set
proj1 (f) is set
proj1 f is set
[:(proj1 f),A:] is Relation-like set
a is set
C . a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
f . a is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
g1 is set
[a,g1] is V22() set
{a,g1} is non empty set
{a} is non empty set
{{a,g1},{a}} is non empty set
[a,g1] `1 is set
[a,g1] `2 is set
(C) . [a,g1] is set
b . g1 is set
t . g1 is set
A is set
B is set
Funcs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
f is Relation-like Function-like set
proj2 f is set
(f) is Relation-like Function-like set
(f) is Relation-like Function-like set
~ (f) is Relation-like Function-like set
proj1 (C) is set
proj1 C is set
[:(proj1 C),A:] is Relation-like set
~ (~ (C)) is Relation-like Function-like set
proj1 (f) is set
proj1 f is set
[:(proj1 f),A:] is Relation-like set
A is set
B is set
Funcs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
((~ (C))) is Relation-like Function-like set
proj1 (C) is set
proj1 C is set
[:(proj1 C),A:] is Relation-like set
f is set
((C)) . f is set
proj2 (C) is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
C . f is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
t is set
(C) . (f,t) is set
[f,t] is V22() set
{f,t} is non empty set
{f} is non empty set
{{f,t},{f}} is non empty set
(C) . [f,t] is set
b . t is set
a . t is set
proj1 ((C)) is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ ((C)) is Relation-like Function-like set
proj2 (C) is set
proj2 C is set
Funcs (A,(proj2 C)) is set
(((C))) is Relation-like Function-like set
~ ((C)) is Relation-like Function-like set
((~ ((C)))) is Relation-like Function-like set
proj1 (C) is set
proj1 ((C)) is set
proj2 (C) is set
Funcs (B,(proj2 C)) is set
(((C))) is Relation-like Function-like set
proj1 (C) is set
proj1 ((C)) is set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ ((C)) is Relation-like Function-like set
b is Relation-like Function-like set
proj1 b is set
f is set
a is set
[:f,a:] is Relation-like set
(b) is Relation-like Function-like set
((b)) is Relation-like Function-like set
proj1 ((b)) is set
t is set
proj1 (b) is set
g1 is set
g is set
[g1,g] is V22() set
{g1,g} is non empty set
{g1} is non empty set
{{g1,g},{g1}} is non empty set
z is Relation-like Function-like set
(b) . g1 is set
proj1 z is set
t is set
t `1 is set
t `2 is set
[(t `1),(t `2)] is V22() set
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
(b) . (t `1) is set
g1 is Relation-like Function-like set
proj1 g1 is set
proj1 (b) is set
t is set
t `1 is set
t `2 is set
[(t `1),(t `2)] is V22() set
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
(b) . (t `1) is set
((b)) . t is set
g1 is Relation-like Function-like set
g1 . (t `2) is set
b . ((t `1),(t `2)) is set
b . [(t `1),(t `2)] is set
((b)) . ((t `1),(t `2)) is set
((b)) . [(t `1),(t `2)] is set
b . t is set
proj1 (~ C) is set
[:B,A:] is Relation-like set
(((~ C))) is Relation-like Function-like set
A is set
B is set
PFuncs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
((~ (C))) is Relation-like Function-like set
proj1 ((C)) is set
proj1 C is set
proj1 (C) is set
[:(proj1 C),A:] is Relation-like set
f is set
C . f is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
the Element of proj1 a is Element of proj1 a
[f, the Element of proj1 a] is V22() set
{f, the Element of proj1 a} is non empty set
{f} is non empty set
{{f, the Element of proj1 a},{f}} is non empty set
proj1 (proj1 (C)) is set
f is set
((C)) . f is set
C . f is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
a is Relation-like Function-like set
proj1 a is set
proj1 (C) is set
{f} is non empty set
proj2 (proj1 (C)) is set
[:{f},(proj2 (proj1 (C))):] is Relation-like set
(proj1 (C)) /\ [:{f},(proj2 (proj1 (C))):] is Relation-like set
proj2 ((proj1 (C)) /\ [:{f},(proj2 (proj1 (C))):]) is set
t is set
g1 is set
[g1,t] is V22() set
{g1,t} is non empty set
{g1} is non empty set
{{g1,t},{g1}} is non empty set
z is set
g2 is set
[z,g2] is V22() set
{z,g2} is non empty set
{z} is non empty set
{{z,g2},{z}} is non empty set
g is Relation-like Function-like set
C . z is set
proj1 g is set
t is set
[f,t] is V22() set
{f,t} is non empty set
{{f,t},{f}} is non empty set
t is set
a . t is set
(C) . (f,t) is set
[f,t] is V22() set
{f,t} is non empty set
{{f,t},{f}} is non empty set
(C) . [f,t] is set
b . t is set
[:(proj1 C),A:] is Relation-like set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
((C)) is Relation-like Function-like set
A is set
B is set
[:A,B:] is Relation-like set
C is Relation-like Function-like set
proj1 C is set
(C) is Relation-like Function-like set
~ C is Relation-like Function-like set
((~ C)) is Relation-like Function-like set
f is Relation-like Function-like set
proj1 f is set
(f) is Relation-like Function-like set
~ f is Relation-like Function-like set
((~ f)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ ((C)) is Relation-like Function-like set
A is set
B is set
PFuncs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
f is Relation-like Function-like set
proj2 f is set
(f) is Relation-like Function-like set
((C)) is Relation-like Function-like set
A is set
B is set
PFuncs (A,B) is set
C is Relation-like Function-like set
proj2 C is set
(C) is Relation-like Function-like set
(C) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
f is Relation-like Function-like set
proj2 f is set
(f) is Relation-like Function-like set
(f) is Relation-like Function-like set
~ (f) is Relation-like Function-like set
((C)) is Relation-like Function-like set
~ (C) is Relation-like Function-like set
((~ (C))) is Relation-like Function-like set
A is set
B is set
C is set
Funcs (C,A) is set
Funcs (C,B) is set
f is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
A is set
Funcs ({},A) is set
B is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
B is set
A is set
card A is cardinal set
B is set
{B} is non empty set
Funcs ({B},A) is set
card (Funcs ({B},A)) is cardinal set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
f is set
C . f is set
a is set
C . a is set
{B} --> f is Relation-like {B} -defined {f} -valued Function-like quasi_total Element of bool [:{B},{f}:]
{f} is non empty set
[:{B},{f}:] is Relation-like non empty set
bool [:{B},{f}:] is non empty set
{B} --> a is Relation-like {B} -defined {a} -valued Function-like quasi_total Element of bool [:{B},{a}:]
{a} is non empty set
[:{B},{a}:] is Relation-like non empty set
bool [:{B},{a}:] is non empty set
({B} --> f) . B is set
f is set
a is set
C . a is set
{B} --> a is Relation-like {B} -defined {a} -valued Function-like quasi_total Element of bool [:{B},{a}:]
{a} is non empty set
[:{B},{a}:] is Relation-like non empty set
bool [:{B},{a}:] is non empty set
dom ({B} --> a) is Element of bool {B}
bool {B} is non empty set
rng ({B} --> a) is Element of bool {a}
bool {a} is non empty set
f is set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
a . B is set
{(a . B)} is non empty set
{B} --> (a . B) is Relation-like {B} -defined {(a . B)} -valued Function-like quasi_total Element of bool [:{B},{(a . B)}:]
[:{B},{(a . B)}:] is Relation-like non empty set
bool [:{B},{(a . B)}:] is non empty set
C . (a . B) is set
A is set
B is set
{B} is non empty set
Funcs (A,{B}) is non empty FUNCTION_DOMAIN of A,{B}
[:A,{B}:] is Relation-like set
bool [:A,{B}:] is non empty set
A --> B is Relation-like A -defined {B} -valued Function-like quasi_total Element of bool [:A,{B}:]
{(A --> B)} is functional non empty Element of bool (bool [:A,{B}:])
bool (bool [:A,{B}:]) is non empty set
C is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
the Element of A is Element of A
{} --> B is Relation-like non-empty empty-yielding {} -defined {B} -valued Function-like one-to-one constant functional empty quasi_total Element of bool [:{},{B}:]
[:{},{B}:] is Relation-like set
bool [:{},{B}:] is non empty set
dom ({} --> B) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty non proper Element of bool {}
bool {} is non empty set
a is set
f . a is set
{(f . a)} is non empty set
a is set
C is set
dom (A --> B) is Element of bool A
bool A is non empty set
rng (A --> B) is Element of bool {B}
bool {B} is non empty set
A is set
B is set
C is set
Funcs (A,C) is set
card (Funcs (A,C)) is cardinal set
f is set
Funcs (B,f) is set
card (Funcs (B,f)) is cardinal set
a is Relation-like Function-like set
proj1 a is set
proj2 a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
a " is Relation-like Function-like set
proj2 (a ") is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
g1 is set
t . g1 is set
z is set
t . z is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
a * g is Relation-like Function-like set
(a * g) * b is Relation-like Function-like set
proj2 (a * g) is set
proj1 (a * g) is set
g2 is Relation-like Function-like set
proj1 g2 is set
proj2 g2 is set
a * g2 is Relation-like Function-like set
proj2 (a * g2) is set
proj1 (a * g2) is set
(a * g2) * b is Relation-like Function-like set
z is set
z9 is set
a . z9 is set
g . z is set
(a * g) . z9 is set
g2 . z is set
g1 is set
z is set
t . z is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
a * g is Relation-like Function-like set
proj1 (a * g) is set
proj2 (a * g) is set
(a * g) * b is Relation-like Function-like set
proj1 ((a * g) * b) is set
proj2 ((a * g) * b) is set
g1 is set
z is Relation-like Function-like set
proj1 z is set
proj2 z is set
b " is Relation-like Function-like set
z * (b ") is Relation-like Function-like set
(a ") * (z * (b ")) is Relation-like Function-like set
a * ((a ") * (z * (b "))) is Relation-like Function-like set
(a * ((a ") * (z * (b ")))) * b is Relation-like Function-like set
a * (a ") is Relation-like Function-like set
(a * (a ")) * (z * (b ")) is Relation-like Function-like set
((a * (a ")) * (z * (b "))) * b is Relation-like Function-like set
(z * (b ")) * b is Relation-like Function-like set
(a * (a ")) * ((z * (b ")) * b) is Relation-like Function-like set
(b ") * b is Relation-like Function-like set
z * ((b ") * b) is Relation-like Function-like set
(a * (a ")) * (z * ((b ") * b)) is Relation-like Function-like set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of bool [:f,f:]
[:f,f:] is Relation-like set
bool [:f,f:] is non empty set
z * (id f) is Relation-like f -valued Function-like set
(a * (a ")) * (z * (id f)) is Relation-like f -valued Function-like set
id B is Relation-like B -defined B -valued Function-like one-to-one total Element of bool [:B,B:]
[:B,B:] is Relation-like set
bool [:B,B:] is non empty set
(id B) * (z * (id f)) is Relation-like B -defined f -valued Function-like set
(id B) * z is Relation-like B -defined Function-like set
proj1 (b ") is set
proj1 (z * (b ")) is set
proj2 (b ") is set
proj2 (z * (b ")) is set
proj2 ((a ") * (z * (b "))) is set
proj1 (a ") is set
proj1 ((a ") * (z * (b "))) is set
t . ((a ") * (z * (b "))) is set
A is set
card A is cardinal set
B is set
card B is cardinal set
C is set
card C is cardinal set
Funcs (A,C) is set
card (Funcs (A,C)) is cardinal set
f is set
card f is cardinal set
Funcs (B,f) is set
card (Funcs (B,f)) is cardinal set
A is set
B is set
A \/ B is set
C is set
Funcs ((A \/ B),C) is set
Funcs (A,C) is set
Funcs (B,C) is set
[:(Funcs (A,C)),(Funcs (B,C)):] is Relation-like set
card (Funcs ((A \/ B),C)) is cardinal set
card [:(Funcs (A,C)),(Funcs (B,C)):] is cardinal set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t | A is Relation-like Function-like set
t | B is Relation-like Function-like set
[(t | A),(t | B)] is V22() set
{(t | A),(t | B)} is functional non empty set
{(t | A)} is functional non empty set
{{(t | A),(t | B)},{(t | A)}} is non empty set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
g1 | A is Relation-like Function-like set
g1 | B is Relation-like Function-like set
[(g1 | A),(g1 | B)] is V22() set
{(g1 | A),(g1 | B)} is functional non empty set
{(g1 | A)} is functional non empty set
{{(g1 | A),(g1 | B)},{(g1 | A)}} is non empty set
z is set
g1 . z is set
(g1 | A) . z is set
t . z is set
(t | A) . z is set
(g1 | B) . z is set
(t | B) . z is set
a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t | B is Relation-like Function-like set
proj2 (t | B) is set
t | A is Relation-like Function-like set
proj2 (t | A) is set
proj1 (t | B) is set
proj1 (t | A) is set
[(t | A),(t | B)] is V22() set
{(t | A),(t | B)} is functional non empty set
{(t | A)} is functional non empty set
{{(t | A),(t | B)},{(t | A)}} is non empty set
a is set
a `1 is set
a `2 is set
[(a `1),(a `2)] is V22() set
{(a `1),(a `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
b +* t is Relation-like Function-like set
proj2 (b +* t) is set
(proj2 b) \/ (proj2 t) is set
C \/ C is set
proj1 (b +* t) is set
f . (b +* t) is set
(b +* t) | A is Relation-like Function-like set
(b +* t) | B is Relation-like Function-like set
[((b +* t) | A),((b +* t) | B)] is V22() set
{((b +* t) | A),((b +* t) | B)} is functional non empty set
{((b +* t) | A)} is functional non empty set
{{((b +* t) | A),((b +* t) | B)},{((b +* t) | A)}} is non empty set
[((b +* t) | A),t] is V22() set
{((b +* t) | A),t} is functional non empty set
{{((b +* t) | A),t},{((b +* t) | A)}} is non empty set
A is set
B is set
[:A,B:] is Relation-like set
C is set
Funcs ([:A,B:],C) is set
Funcs (B,C) is set
Funcs (A,(Funcs (B,C))) is set
card (Funcs ([:A,B:],C)) is cardinal set
card (Funcs (A,(Funcs (B,C)))) is cardinal set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
(t) is Relation-like Function-like set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
(g1) is Relation-like Function-like set
a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
(t) is Relation-like Function-like set
proj1 (t) is set
proj2 (t) is set
Funcs (B,(proj2 t)) is set
a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
(b) is Relation-like Function-like set
proj1 (b) is set
proj2 (b) is set
((b)) is Relation-like Function-like set
f . (b) is set
[:A,{{}}:] is Relation-like set
bool [:A,{{}}:] is non empty set
A --> {} is Relation-like A -defined {{}} -valued Function-like quasi_total Element of bool [:A,{{}}:]
{(A --> {})} is functional non empty Element of bool (bool [:A,{{}}:])
bool (bool [:A,{{}}:]) is non empty set
A is set
B is set
Funcs (A,B) is set
C is set
[:B,C:] is Relation-like set
Funcs (A,[:B,C:]) is set
Funcs (A,C) is set
[:(Funcs (A,B)),(Funcs (A,C)):] is Relation-like set
card (Funcs (A,[:B,C:])) is cardinal set
card [:(Funcs (A,B)),(Funcs (A,C)):] is cardinal set
pr1 (B,C) is Relation-like [:B,C:] -defined B -valued Function-like quasi_total Element of bool [:[:B,C:],B:]
[:[:B,C:],B:] is Relation-like set
bool [:[:B,C:],B:] is non empty set
pr2 (B,C) is Relation-like [:B,C:] -defined C -valued Function-like quasi_total Element of bool [:[:B,C:],C:]
[:[:B,C:],C:] is Relation-like set
bool [:[:B,C:],C:] is non empty set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
t * (pr1 (B,C)) is Relation-like B -valued Function-like set
t * (pr2 (B,C)) is Relation-like C -valued Function-like set
[(t * (pr1 (B,C))),(t * (pr2 (B,C)))] is V22() set
{(t * (pr1 (B,C))),(t * (pr2 (B,C)))} is functional non empty set
{(t * (pr1 (B,C)))} is functional non empty set
{{(t * (pr1 (B,C))),(t * (pr2 (B,C)))},{(t * (pr1 (B,C)))}} is non empty set
g1 * (pr1 (B,C)) is Relation-like B -valued Function-like set
g1 * (pr2 (B,C)) is Relation-like C -valued Function-like set
[(g1 * (pr1 (B,C))),(g1 * (pr2 (B,C)))] is V22() set
{(g1 * (pr1 (B,C))),(g1 * (pr2 (B,C)))} is functional non empty set
{(g1 * (pr1 (B,C)))} is functional non empty set
{{(g1 * (pr1 (B,C))),(g1 * (pr2 (B,C)))},{(g1 * (pr1 (B,C)))}} is non empty set
z is set
(t * (pr2 (B,C))) . z is set
t . z is set
(pr2 (B,C)) . (t . z) is set
g1 . z is set
(g1 . z) `1 is set
(g1 . z) `2 is set
[((g1 . z) `1),((g1 . z) `2)] is V22() set
{((g1 . z) `1),((g1 . z) `2)} is non empty set
{((g1 . z) `1)} is non empty set
{{((g1 . z) `1),((g1 . z) `2)},{((g1 . z) `1)}} is non empty set
(t . z) `1 is set
(t . z) `2 is set
[((t . z) `1),((t . z) `2)] is V22() set
{((t . z) `1),((t . z) `2)} is non empty set
{((t . z) `1)} is non empty set
{{((t . z) `1),((t . z) `2)},{((t . z) `1)}} is non empty set
(pr1 (B,C)) . (((g1 . z) `1),((g1 . z) `2)) is set
(pr1 (B,C)) . [((g1 . z) `1),((g1 . z) `2)] is set
(pr2 (B,C)) . (((g1 . z) `1),((g1 . z) `2)) is set
(pr2 (B,C)) . [((g1 . z) `1),((g1 . z) `2)] is set
(pr1 (B,C)) . (((t . z) `1),((t . z) `2)) is set
(pr1 (B,C)) . [((t . z) `1),((t . z) `2)] is set
(pr2 (B,C)) . (((t . z) `1),((t . z) `2)) is set
(pr2 (B,C)) . [((t . z) `1),((t . z) `2)] is set
(t * (pr1 (B,C))) . z is set
(pr1 (B,C)) . (t . z) is set
(g1 * (pr1 (B,C))) . z is set
(pr1 (B,C)) . (g1 . z) is set
a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t * (pr1 (B,C)) is Relation-like B -valued Function-like set
rng (t * (pr1 (B,C))) is Element of bool B
bool B is non empty set
t * (pr2 (B,C)) is Relation-like C -valued Function-like set
rng (t * (pr2 (B,C))) is Element of bool C
bool C is non empty set
dom (pr2 (B,C)) is Relation-like B -defined C -valued Element of bool [:B,C:]
bool [:B,C:] is non empty set
proj1 (t * (pr2 (B,C))) is set
dom (pr1 (B,C)) is Relation-like B -defined C -valued Element of bool [:B,C:]
proj1 (t * (pr1 (B,C))) is set
[(t * (pr1 (B,C))),(t * (pr2 (B,C)))] is V22() set
{(t * (pr1 (B,C))),(t * (pr2 (B,C)))} is functional non empty set
{(t * (pr1 (B,C)))} is functional non empty set
{{(t * (pr1 (B,C))),(t * (pr2 (B,C)))},{(t * (pr1 (B,C)))}} is non empty set
a is set
a `1 is set
a `2 is set
[(a `1),(a `2)] is V22() set
{(a `1),(a `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
<:t,b:> is Relation-like Function-like set
proj2 <:t,b:> is set
[:(proj2 t),(proj2 b):] is Relation-like set
proj1 <:t,b:> is set
A /\ A is set
<:t,b:> * (pr1 (B,C)) is Relation-like B -valued Function-like set
<:t,b:> * (pr2 (B,C)) is Relation-like C -valued Function-like set
f . <:t,b:> is set
[t,b] is V22() set
{t,b} is functional non empty set
{t} is functional non empty set
{{t,b},{t}} is non empty set
A is set
B is set
{A,B} is non empty set
C is set
Funcs (C,{A,B}) is non empty FUNCTION_DOMAIN of C,{A,B}
bool C is non empty set
card (Funcs (C,{A,B})) is cardinal set
card (bool C) is cardinal set
{A} is non empty set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t " {A} is set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
g1 " {A} is set
z is set
g1 . z is set
t . z is set
a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t " {A} is set
a is set
b is Relation-like Function-like set
proj1 b is set
b " {A} is set
t is set
b . t is set
t is set
b . t is set
proj2 b is set
t is set
g1 is set
b . g1 is set
f . b is set
A is set
B is set
{A,B} is non empty set
C is set
Funcs ({A,B},C) is set
[:C,C:] is Relation-like set
card (Funcs ({A,B},C)) is cardinal set
card [:C,C:] is cardinal set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
g1 is Relation-like Function-like set
proj1 g1 is set
proj2 g1 is set
g1 . A is set
g1 . B is set
[(g1 . A),(g1 . B)] is V22() set
{(g1 . A),(g1 . B)} is non empty set
{(g1 . A)} is non empty set
{{(g1 . A),(g1 . B)},{(g1 . A)}} is non empty set
t . A is set
t . B is set
[(t . A),(t . B)] is V22() set
{(t . A),(t . B)} is non empty set
{(t . A)} is non empty set
{{(t . A),(t . B)},{(t . A)}} is non empty set
z is set
g1 . z is set
t . z is set
a is set
b is set
f . b is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t . A is set
t . B is set
[(t . A),(t . B)] is V22() set
{(t . A),(t . B)} is non empty set
{(t . A)} is non empty set
{{(t . A),(t . B)},{(t . A)}} is non empty set
a is set
a `1 is set
a `2 is set
b is Relation-like Function-like set
proj1 b is set
b . A is set
b . B is set
[(a `1),(a `2)] is V22() set
{(a `1),(a `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
proj2 b is set
t is set
g1 is set
b . g1 is set
f . b is set
[(b . A),(b . B)] is V22() set
{(b . A),(b . B)} is non empty set
{(b . A)} is non empty set
{{(b . A),(b . B)},{(b . A)}} is non empty set
{} .--> {} is set
{{}} --> {} is Relation-like {{}} -defined {{}} -valued Function-like quasi_total Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like non empty set
bool [:{{}},{{}}:] is non empty set
({},{}) :-> {} is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like quasi_total Element of bool [:[:{{}},{{}}:],{{}}:]
[:[:{{}},{{}}:],{{}}:] is Relation-like non empty set
bool [:[:{{}},{{}}:],{{}}:] is non empty set
[{},{}] is V22() set
{{},{}} is functional non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is Relation-like Function-like non empty set
{[{},{}]} --> {} is Relation-like {[{},{}]} -defined {{}} -valued Function-like quasi_total Element of bool [:{[{},{}]},{{}}:]
[:{[{},{}]},{{}}:] is Relation-like non empty set
bool [:{[{},{}]},{{}}:] is non empty set
() is set
() is set
[:1,1:] is Relation-like non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is Relation-like non empty set
bool [:[:1,1:],1:] is non empty set
B is set
C is non empty set
A is non empty set
f is non empty FUNCTION_DOMAIN of B,C
[:A,f:] is Relation-like non empty set
bool [:A,f:] is non empty set
a is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]
b is Element of A
a . b is set
a . b is Element of f
A is non empty set
B is non empty set
[:A,B:] is Relation-like non empty set
C is non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
f is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
(f) is Relation-like Function-like set
dom f is Relation-like A -defined B -valued Element of bool [:A,B:]
bool [:A,B:] is non empty set
proj2 (f) is set
rng f is Element of bool C
bool C is non empty set
Funcs (B,(rng f)) is set
a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
[:B,C:] is Relation-like non empty set
bool [:B,C:] is non empty set
proj1 (f) is set
A is non empty set
B is non empty set
[:B,A:] is Relation-like non empty set
C is non empty set
[:[:B,A:],C:] is Relation-like non empty set
bool [:[:B,A:],C:] is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
f is Relation-like [:B,A:] -defined C -valued Function-like quasi_total Element of bool [:[:B,A:],C:]
(f) is Relation-like Function-like set
~ f is Relation-like Function-like set
((~ f)) is Relation-like Function-like set
dom f is Relation-like B -defined A -valued Element of bool [:B,A:]
bool [:B,A:] is non empty set
proj2 (f) is set
rng f is Element of bool C
bool C is non empty set
Funcs (B,(rng f)) is set
a is set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
[:B,C:] is Relation-like non empty set
bool [:B,C:] is non empty set
proj1 (f) is set
A is non empty set
B is non empty set
[:A,B:] is Relation-like non empty set
C is non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
f is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
(f) is Relation-like Function-like set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
(f) is Relation-like Function-like set
~ f is Relation-like Function-like set
((~ f)) is Relation-like Function-like set
Funcs (A,C) is non empty FUNCTION_DOMAIN of A,C
[:B,(Funcs (A,C)):] is Relation-like non empty set
bool [:B,(Funcs (A,C)):] is non empty set
A is non empty set
B is non empty set
[:A,B:] is Relation-like non empty set
C is non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
f is Element of A
a is Element of B
b is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
b . (f,a) is Element of C
[f,a] is V22() set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
b . [f,a] is set
(A,B,C,b) is Relation-like A -defined Funcs (B,C) -valued Function-like quasi_total Element of bool [:A,(Funcs (B,C)):]
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
(A,B,C,(Funcs (B,C)),(A,B,C,b),f) is Relation-like B -defined C -valued Function-like quasi_total Element of Funcs (B,C)
(A,B,C,(Funcs (B,C)),(A,B,C,b),f) . a is Element of C
[f,a] is V22() Element of [:A,B:]
dom b is Relation-like A -defined B -valued Element of bool [:A,B:]
bool [:A,B:] is non empty set
A is non empty set
B is non empty set
[:A,B:] is Relation-like non empty set
C is non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
Funcs (A,C) is non empty FUNCTION_DOMAIN of A,C
f is Element of A
a is Element of B
b is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
b . (f,a) is Element of C
[f,a] is V22() set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
b . [f,a] is set
(A,B,C,b) is Relation-like B -defined Funcs (A,C) -valued Function-like quasi_total Element of bool [:B,(Funcs (A,C)):]
[:B,(Funcs (A,C)):] is Relation-like non empty set
bool [:B,(Funcs (A,C)):] is non empty set
~ b is Relation-like Function-like set
((~ b)) is Relation-like Function-like set
(B,A,C,(Funcs (A,C)),(A,B,C,b),a) is Relation-like A -defined C -valued Function-like quasi_total Element of Funcs (A,C)
(B,A,C,(Funcs (A,C)),(A,B,C,b),a) . f is Element of C
[f,a] is V22() Element of [:A,B:]
dom b is Relation-like A -defined B -valued Element of bool [:A,B:]
bool [:A,B:] is non empty set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
f is Relation-like A -defined Funcs (B,C) -valued Function-like quasi_total Element of bool [:A,(Funcs (B,C)):]
(f) is Relation-like Function-like set
[:A,B:] is Relation-like non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
rng f is Element of bool (Funcs (B,C))
bool (Funcs (B,C)) is non empty set
proj2 (f) is set
proj1 (f) is set
dom f is Element of bool A
bool A is non empty set
[:(dom f),B:] is Relation-like set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
f is Relation-like A -defined Funcs (B,C) -valued Function-like quasi_total Element of bool [:A,(Funcs (B,C)):]
(A,B,C,f) is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
[:A,B:] is Relation-like non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
(A,B,C,(A,B,C,f)) is Relation-like A -defined Funcs (B,C) -valued Function-like quasi_total Element of bool [:A,(Funcs (B,C)):]
rng f is Element of bool (Funcs (B,C))
bool (Funcs (B,C)) is non empty set
A is non empty set
B is non empty set
C is non empty set
Funcs (B,C) is non empty FUNCTION_DOMAIN of B,C
[:A,(Funcs (B,C)):] is Relation-like non empty set
bool [:A,(Funcs (B,C)):] is non empty set
f is Relation-like A -defined Funcs (B,C) -valued Function-like quasi_total Element of bool [:A,(Funcs (B,C)):]
(A,B,C,f) is Relation-like [:A,B:] -defined C -valued Function-like quasi_total Element of bool [:[:A,B:],C:]
[:A,B:] is Relation-like non empty set
[:[:A,B:],C:] is Relation-like non empty set
bool [:[:A,B:],C:] is non empty set
a is Element of A
(A,B,C,(Funcs (B,C)),f,a) is Relation-like B -defined C -valued Function-like quasi_total Element of Funcs (B,C)
b is Element of B
(A,B,C,f) . (a,b) is Element of C
[a,b] is V22() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
(A,B,C,f) . [a,b] is set
(A,B,C,(Funcs (B,C)),f,a) . b is Element of C
dom f is Element of bool A
bool A is non empty set
dom (A,B,C,(Funcs (B,C)),f,a) is Element of bool B
bool B is non empty set