:: FUNCT_5 semantic presentation

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

F

A is Relation-like Function-like set

proj1 A is set

B is Relation-like Function-like set

A . B is set

F

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