:: FUNCT_5 semantic presentation

1 is non empty set
{{},1} is non empty set
K47() is set
bool K47() is non empty set

F1() is set

proj1 A is set

A . B is set
F2(B) is set

proj1 () is 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

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

proj2 {[A,B]} is non empty set
{B} is 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

proj1 A is set
proj1 () is set

proj1 (~ A) is set
proj2 (proj1 (~ A)) is set
proj2 () 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

proj1 A is set

proj2 B is set

proj1 A is set
proj1 () is set
proj2 () is set
B is set
{B} is non empty set
[:{B},(proj2 ()):] is Relation-like set
() /\ [:{B},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{B},(proj2 ()):]) is set
C is set
f is set

proj1 a is 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 ()):] is Relation-like set
() /\ [:{B},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{B},(proj2 ()):]) is 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

proj1 B is set

proj1 B is set

proj1 C is set
f is set
B . f is set
{f} is non empty set
[:{f},(proj2 ()):] is Relation-like set
() /\ [:{f},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{f},(proj2 ()):]) is set

proj1 a is set
C . f is 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

proj1 C is set
proj2 C is set
union () is set
[:B,(union ()):] is Relation-like set
f is set
a is set
a `1 is set
A . (a `1) is set
a `2 is set

b . (a `2) is set
a is set

a `1 is set
A . (a `1) is set
b is set
a `2 is set
g1 . (a `2) is set

t is set
z . (a `2) is set

proj1 a is set
b is set
b `1 is set
t is set
A . t is 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

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

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 . (b `2) is set

g1 . (b `2) is set

proj1 B is 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

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

proj1 C is set

proj1 (C) is set
(C) . A is set
proj1 () is set
proj2 () is set
[:{A},(proj2 ()):] is Relation-like set
() /\ [:{A},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{A},(proj2 ()):]) is 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

proj1 C is set

(C) . A is set
C . (A,B) is set
C . [A,B] is set

proj1 f is set
f . B is set
proj1 () is set
proj2 () is set
[:{A},(proj2 ()):] is Relation-like set
() /\ [:{A},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{A},(proj2 ()):]) is set

proj1 a is 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

proj1 C is 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

proj1 C is set

((~ C)) is Relation-like Function-like set
(C) . B is set
C . (A,B) is set
C . [A,B] is 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
proj1 (A) is set
proj1 A is set
proj2 () 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

proj1 C is set

proj1 (C) is set

((~ C)) is Relation-like Function-like set
proj1 (C) is set
proj1 () 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

proj1 C is set

proj1 (C) is set

((~ C)) is Relation-like Function-like set
proj1 (C) is set
proj1 () 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

proj2 C is set

proj1 (C) is set
proj1 C is set
[:(),A:] is Relation-like set

proj1 (C) is set
[:A,():] is Relation-like set
f is set
f `1 is set
C . (f `1) is 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

C . a is set
proj1 b is 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

C . b is set
proj1 t is set

proj1 A is set

((~ A)) is Relation-like Function-like set
proj1 () 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

proj1 A is 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

A . C is set
proj1 f is set
A is set
B is set
[:A,B:] is Relation-like set
C is set

proj1 f is set

(f) . C is set
proj2 f is set
{C} is non empty set

[:{C},B:] /\ () is Relation-like set
proj1 () is set
proj2 () is set
[:{C},(proj2 ()):] is Relation-like set
() /\ [:{C},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{C},(proj2 ()):]) is 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

proj1 (B) is set
(B) . A is set
proj1 B is set
proj1 () is set
{A} is non empty set
proj2 () is set
[:{A},(proj2 ()):] is Relation-like set
() /\ [:{A},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{A},(proj2 ()):]) is set

proj1 C is set
A is set
{A} is non empty set

proj1 (B) is set
(B) . A is set
proj1 B is set
proj2 () is set
[:{A},(proj2 ()):] is Relation-like set
() /\ [:{A},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{A},(proj2 ()):]) is set
proj2 B is set

proj1 C is set
proj2 C is set
proj1 () is 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

proj1 f is 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

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
proj1 (B) is set
(B) . A is set
A is set
{A} is non empty set

((~ B)) is Relation-like Function-like set
proj1 (B) is set
(B) . A is set
proj1 B is set
proj1 () is set
[:(proj1 ()),{A}:] is Relation-like set
() /\ [:(proj1 ()),{A}:] is Relation-like set
proj1 (() /\ [:(proj1 ()),{A}:]) is set
proj2 B is 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 ()):] is Relation-like set
(proj1 (~ B)) /\ [:{A},(proj1 ()):] is Relation-like set
proj2 ((proj1 (~ B)) /\ [:{A},(proj1 ()):]) 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

proj1 C is set

proj2 (C) is set
proj2 C is set
Funcs (B,()) is set

((~ C)) is Relation-like Function-like set
proj2 (C) is set
Funcs (A,()) is set
proj1 (C) is set
f is set
a is set
(C) . a is set

proj1 b is set
proj2 b is set
proj1 (C) is set
f is set
a is set
(C) . a is 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

proj2 (A) is set
proj1 A is set
proj2 () is set
proj2 A is set
PFuncs ((proj2 ()),()) is set

((~ A)) is Relation-like Function-like set
proj2 (A) is set
proj1 () is set
PFuncs ((proj1 ()),()) 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 ()):] is Relation-like set
() /\ [:{C},(proj2 ()):] is Relation-like set
proj2 (() /\ [:{C},(proj2 ()):]) is 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

proj1 f is set
proj2 f is set
A is set
B is set
PFuncs (A,B) is set

proj2 C is set

proj1 (C) is set
proj1 C is set
[:(),A:] is Relation-like set

proj1 (C) is set
[:A,():] 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

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

proj1 C is set
C . A is set

proj1 (C) is set
(C) . (A,B) is set
(C) . [A,B] is set
proj2 (C) is 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

proj1 C is set
C . A is set

proj1 (C) is set
(C) . (B,A) is set
(C) . [B,A] is set
proj2 (C) is 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

proj2 C is set

proj2 (C) is 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

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

proj1 z is set
proj2 z is set
A is set
B is set
Funcs (A,B) is set

proj2 C is set

proj2 (C) is set

proj2 (C) is set
PFuncs (A,B) is set

(()) is Relation-like Function-like set
proj1 ({}) is 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

proj1 C is set
A is set
B is set
[:A,B:] is Relation-like set

proj1 C is set

proj1 f is set

a is set
a `1 is set
(C) . (a `1) is set
proj2 C is 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

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

proj1 C is set

((~ C)) is Relation-like Function-like set

proj1 f is set

((~ f)) is Relation-like Function-like set
proj1 (~ C) is set
[:B,A:] is Relation-like set
proj1 (~ f) is set

A is set
B is set
Funcs (A,B) is set

proj2 C is set

proj2 f is set

proj1 (C) is set
proj1 C is set
[:(),A:] is Relation-like set
proj1 (f) is set
proj1 f is set
[:(),A:] is Relation-like set
a is set
C . a is set

proj1 b is set
proj2 b is set
f . a is 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

proj2 C is set

proj2 f is set

proj1 (C) is set
proj1 C is set
[:(),A:] is Relation-like set
~ (~ (C)) is Relation-like Function-like set
proj1 (f) is set
proj1 f is set
[:(),A:] is Relation-like set
A is set
B is set
Funcs (A,B) is 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
proj1 (C) is set
proj1 C is set
[:(),A:] is Relation-like set
f is set
((C)) . f is set
proj2 (C) is set

proj1 a is set
proj2 a is set
C . f is 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

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
proj2 (C) is set
proj2 C is set
Funcs (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
proj1 ((C)) is set
proj2 (C) is set
Funcs (B,()) 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

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

proj1 b is set
f is set
a is set
[:f,a:] is Relation-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

(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

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

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
proj1 (C) is set
[:(),A:] is Relation-like set
f is set
C . f is 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

proj1 b is set
proj2 b is 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

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
[:(),A:] is Relation-like set
A is set
B is set
[:A,B:] is Relation-like set

proj1 C is set

proj1 f is set

((C)) is Relation-like Function-like set
A is set
B is set
[:A,B:] is Relation-like set

proj1 C is set

((~ C)) is Relation-like Function-like set

proj1 f is 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

proj2 C is set

proj2 f is set

((C)) is Relation-like Function-like set
A is set
B is set
PFuncs (A,B) is set

proj2 C is set

proj2 f is 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

proj1 a is set
proj2 a is set
A is set
Funcs ({},A) is set
B is set

proj1 C is set
proj2 C is set
B is set
A is set

B is set
{B} is non empty set
Funcs ({B},A) is set
card (Funcs ({B},A)) is cardinal set

proj1 C is set
proj2 C is set
f is set
C . f is set
a is set
C . a is set

{f} is non empty set
[:{B},{f}:] is Relation-like non empty set
bool [:{B},{f}:] is non empty set

{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

{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

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}

bool [:A,{B}:] is non empty set

{(A --> B)} is functional non empty Element of bool (bool [:A,{B}:])
bool (bool [:A,{B}:]) is non empty set
C is set

proj1 f is set
proj2 f is set
the Element of A is Element of A

bool [:{},{B}:] is non empty set

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

proj1 a is set
proj2 a is set

proj1 b is set
proj2 b is set

proj2 (a ") is set

proj1 t is set
proj2 t is set
g1 is set
t . g1 is set
z is set
t . z is set

proj1 g is set
proj2 g is set

(a * g) * b is Relation-like Function-like set
proj2 (a * g) is set
proj1 (a * g) is set

proj1 g2 is set
proj2 g2 is 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

proj1 g is set
proj2 g is 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

proj1 z is set
proj2 z is 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 ")) * (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

z * ((b ") * b) is Relation-like Function-like set
(a * (a ")) * (z * ((b ") * b)) is Relation-like Function-like set

[:f,f:] is Relation-like set
bool [:f,f:] is non empty set

(a * (a ")) * (z * (id f)) is Relation-like f -valued Function-like set

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

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

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

proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set

proj1 t is set
proj2 t 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

proj1 g1 is set
proj2 g1 is 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

proj1 t is set
proj2 t is set

proj2 (t | B) is 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

proj1 b is set
proj2 b is set

proj1 t is set
proj2 t is set

proj2 (b +* t) is set
() \/ () 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

proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set

proj1 t is set
proj2 t is set

proj1 g1 is set
proj2 g1 is set

a is set
b is set
f . b is set

proj1 t is set
proj2 t is set

proj1 (t) is set
proj2 (t) is set
Funcs (B,()) is set
a is set

proj1 b is set
proj2 b is set

proj1 (b) is set
proj2 (b) is set
((b)) is Relation-like Function-like set
f . (b) is set

bool [:A,:] is non empty set

{()} is functional non empty Element of bool ()
bool () 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

[:[:B,C:],B:] is Relation-like set
bool [:[:B,C:],B:] is non empty set

[:[:B,C:],C:] is Relation-like set
bool [:[:B,C:],C:] is non empty set

proj1 f is set
proj2 f is set
a is set
f . a is set
b is set
f . b is set

proj1 t is set
proj2 t is 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

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