:: FUNCTOR0 semantic presentation

K141() is Element of bool K137()

K137() is set

bool K137() is non empty set

{} is set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

1 is non empty set

{{},1} is set

K103() is set

bool K103() is non empty set

bool K141() is non empty set

F

F

{ [[b

F

F

F

[F

{F

{F

{{F

F

F

[:F

{ [b

{ [b

A is set

B is Element of F

A is Element of F

[B,A] is V15() set

{B,A} is set

{B} is set

{{B,A},{B}} is set

F

[[B,A],F

{[B,A],F

{[B,A]} is Relation-like Function-like set

{{[B,A],F

B is Element of [:F

B `1 is set

B `2 is set

A is set

B is Element of [:F

B `1 is set

B `2 is set

F

[B,F

{B,F

{B} is set

{{B,F

A is Element of F

B is Element of F

[A,B] is V15() set

{A,B} is set

{A} is set

{{A,B},{A}} is set

A is Element of [:F

A `1 is set

A `2 is set

F

F

A is set

[:A,{}:] is Relation-like set

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

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) quasi_total Element of bool [:A,A:]

[:A,A:] is Relation-like set

bool [:A,A:] is non empty set

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

(id A) * B is Relation-like A -defined Function-like set

dom B is Element of bool A

bool A is non empty set

A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

~ A is Relation-like Function-like Function-yielding V37() set

proj2 A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V37() set

proj2 (~ A) is set

B is Relation-like Function-like set

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

proj1 A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

proj1 [:A,B:] is set

proj1 B is set

[:{},(proj1 B):] is Relation-like set

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

proj1 A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

proj1 [:B,A:] is set

proj1 B is set

[:(proj1 B),{}:] is Relation-like set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) quasi_total Element of bool [:A,A:]

[:A,A:] is Relation-like set

bool [:A,A:] is non empty set

B is Relation-like Function-like set

B .: (id A) is set

~ B is Relation-like Function-like set

(~ B) .: (id A) is set

A is set

proj1 B is set

B is set

B . B is set

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

proj1 (~ B) is set

B . (F,G) is set

B . [F,G] is set

(~ B) . (F,G) is set

(~ B) . [F,G] is set

A is set

proj1 (~ B) is set

B is set

(~ B) . B is set

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

proj1 B is set

(~ B) . (F,G) is set

(~ B) . [F,G] is set

B . (F,G) is set

B . [F,G] is set

A is set

B is set

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

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

[:B,B:] is Relation-like set

A is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]

[:A,A:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

[:A,A:] is Relation-like set

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

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

rng [:A,A:] is Relation-like B -defined B -valued Element of bool [:B,B:]

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

rng A is Element of bool B

bool B is non empty set

[:(rng A),(rng A):] is Relation-like B -defined B -valued Element of bool [:B,B:]

A is Relation-like Function-like Function-yielding V37() set

~ A is Relation-like Function-like Function-yielding V37() set

A is set

B is set

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

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

A is set

[:A,B:] --> A is Relation-like [:A,B:] -defined {A} -valued Function-like constant V14([:A,B:]) quasi_total Element of bool [:[:A,B:],{A}:]

{A} is set

[:[:A,B:],{A}:] is Relation-like set

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

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

[:B,A:] --> A is Relation-like [:B,A:] -defined {A} -valued Function-like constant V14([:B,A:]) quasi_total Element of bool [:[:B,A:],{A}:]

[:[:B,A:],{A}:] is Relation-like set

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

B is set

dom ([:B,A:] --> A) is Relation-like B -defined A -valued Element of bool [:B,A:]

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

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

o2 is set

c

[o2,c

{o2,c

{o2} is set

{{o2,c

[c

{c

{c

{{c

dom ([:A,B:] --> A) is Relation-like A -defined B -valued Element of bool [:A,B:]

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

G is set

F is set

[G,F] is V15() set

{G,F} is set

{G} is set

{{G,F},{G}} is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

B is set

F is set

[B,F] is V15() set

{B,F} is set

{B} is set

{{B,F},{B}} is set

([:B,A:] --> A) . (F,B) is set

[F,B] is V15() set

{F,B} is set

{F} is set

{{F,B},{F}} is set

([:B,A:] --> A) . [F,B] is set

([:A,B:] --> A) . (B,F) is set

([:A,B:] --> A) . [B,F] is set

A is Relation-like Function-like set

B is Relation-like Function-like set

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

[:A,B:] " is Relation-like Function-like set

A " is Relation-like Function-like set

B " is Relation-like Function-like set

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

proj1 (A ") is set

proj2 A is set

proj1 (B ") is set

proj2 B is set

proj1 ([:A,B:] ") is set

proj2 [:A,B:] is set

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

A is set

B is set

([:A,B:] ") . (A,B) is set

[A,B] is V15() set

{A,B} is set

{A} is set

{{A,B},{A}} is set

([:A,B:] ") . [A,B] is set

(A ") . A is set

(B ") . B is set

[((A ") . A),((B ") . B)] is V15() set

{((A ") . A),((B ") . B)} is set

{((A ") . A)} is set

{{((A ") . A),((B ") . B)},{((A ") . A)}} is set

proj1 [:A,B:] is set

proj1 A is set

proj1 B is set

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

proj2 (A ") is set

proj2 (B ") is set

A . ((A ") . A) is set

(A ") * A is Relation-like Function-like set

((A ") * A) . A is set

(A ") " is Relation-like Function-like set

(A ") * ((A ") ") is Relation-like Function-like set

((A ") * ((A ") ")) . A is set

id (proj1 (A ")) is Relation-like proj1 (A ") -defined proj1 (A ") -valued Function-like one-to-one V14( proj1 (A ")) quasi_total Element of bool [:(proj1 (A ")),(proj1 (A ")):]

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

bool [:(proj1 (A ")),(proj1 (A ")):] is non empty set

(id (proj1 (A "))) . A is set

B . ((B ") . B) is set

(B ") * B is Relation-like Function-like set

((B ") * B) . B is set

(B ") " is Relation-like Function-like set

(B ") * ((B ") ") is Relation-like Function-like set

((B ") * ((B ") ")) . B is set

id (proj1 (B ")) is Relation-like proj1 (B ") -defined proj1 (B ") -valued Function-like one-to-one V14( proj1 (B ")) quasi_total Element of bool [:(proj1 (B ")),(proj1 (B ")):]

[:(proj1 (B ")),(proj1 (B ")):] is Relation-like set

bool [:(proj1 (B ")),(proj1 (B ")):] is non empty set

(id (proj1 (B "))) . B is set

[:A,B:] . (((A ") . A),((B ") . B)) is set

[:A,B:] . [((A ") . A),((B ") . B)] is set

A is Relation-like Function-like set

[:A,A:] is Relation-like Function-like set

B is set

proj1 A is set

A is set

A . B is set

A . A is set

proj1 [:A,A:] is set

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

[B,B] is V15() set

{B,B} is set

{B} is set

{{B,B},{B}} is set

[A,A] is V15() set

{A,A} is set

{A} is set

{{A,A},{A}} is set

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

[:A,A:] . [B,B] is set

[(A . A),(A . A)] is V15() set

{(A . A),(A . A)} is set

{(A . A)} is set

{{(A . A),(A . A)},{(A . A)}} is set

[:A,A:] . (A,A) is set

[:A,A:] . [A,A] is set

A is Relation-like Function-like set

~ A is Relation-like Function-like set

B is set

proj1 (~ A) is set

A is set

(~ A) . B is set

(~ A) . A is set

B is set

F is set

[:B,F:] is Relation-like set

G is set

c

[G,c

{G,c

{G} is set

{{G,c

o2 is set

o3 is set

[o2,o3] is V15() set

{o2,o3} is set

{o2} is set

{{o2,o3},{o2}} is set

[c

{c

{c

{{c

proj1 A is set

[o3,o2] is V15() set

{o3,o2} is set

{o3} is set

{{o3,o2},{o3}} is set

A . (c

A . [c

(~ A) . (G,c

(~ A) . [G,c

(~ A) . (o2,o3) is set

(~ A) . [o2,o3] is set

A . (o3,o2) is set

A . [o3,o2] is set

A is Relation-like Function-like set

B is Relation-like Function-like set

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

~ [:A,B:] is Relation-like Function-like set

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

A is set

proj1 [:B,A:] is set

B is set

[:B,A:] . A is set

[:B,A:] . B is set

proj1 B is set

proj1 A is set

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

proj1 [:A,B:] is set

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

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

c

o2 is set

[c

{c

{c

{{c

proj1 (~ [:A,B:]) is set

[:B,A:] . (F,G) is set

[:B,A:] . [F,G] is set

B . F is set

A . G is set

[(B . F),(A . G)] is V15() set

{(B . F),(A . G)} is set

{(B . F)} is set

{{(B . F),(A . G)},{(B . F)}} is set

[:B,A:] . (c

[:B,A:] . [c

B . c

A . o2 is set

[(B . c

{(B . c

{(B . c

{{(B . c

(~ [:A,B:]) . [F,G] is set

(~ [:A,B:]) . (F,G) is set

[:A,B:] . (G,F) is set

[G,F] is V15() set

{G,F} is set

{G} is set

{{G,F},{G}} is set

[:A,B:] . [G,F] is set

[(A . o2),(B . c

{(A . o2),(B . c

{(A . o2)} is set

{{(A . o2),(B . c

[:A,B:] . (o2,c

[o2,c

{o2,c

{o2} is set

{{o2,c

[:A,B:] . [o2,c

(~ [:A,B:]) . (c

(~ [:A,B:]) . [c

A is Relation-like Function-like set

B is Relation-like Function-like set

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

~ [:A,B:] is Relation-like Function-like set

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

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

[:B,A:] " is Relation-like Function-like set

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

B " is Relation-like Function-like set

A " is Relation-like Function-like set

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

proj1 ([:B,A:] ") is set

proj1 (B ") is set

proj1 (A ") is set

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

proj1 [:A,B:] is set

proj1 A is set

proj1 B is set

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

proj1 [:B,A:] is set

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

[:A,B:] " is Relation-like Function-like set

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

proj1 (~ ([:B,A:] ")) is set

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

proj1 [:(A "),(B "):] is set

proj2 [:A,B:] is set

proj2 (~ [:A,B:]) is set

A is set

B is set

(~ ([:B,A:] ")) . A is set

proj2 A is set

proj2 B is set

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

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

(A ") . F is set

(B ") . G is set

[G,F] is V15() set

{G,F} is set

{G} is set

{{G,F},{G}} is set

(~ ([:B,A:] ")) . (F,G) is set

(~ ([:B,A:] ")) . [F,G] is set

[:(B "),(A "):] . (G,F) is set

[:(B "),(A "):] . [G,F] is set

[((B ") . G),((A ") . F)] is V15() set

{((B ") . G),((A ") . F)} is set

{((B ") . G)} is set

{{((B ") . G),((A ") . F)},{((B ") . G)}} is set

proj2 (A ") is set

proj2 (B ") is set

proj1 (~ [:A,B:]) is set

A . ((A ") . F) is set

B . ((B ") . G) is set

(~ [:A,B:]) . B is set

(~ [:A,B:]) . (((B ") . G),((A ") . F)) is set

(~ [:A,B:]) . [((B ") . G),((A ") . F)] is set

[:A,B:] . (((A ") . F),((B ") . G)) is set

[((A ") . F),((B ") . G)] is V15() set

{((A ") . F),((B ") . G)} is set

{((A ") . F)} is set

{{((A ") . F),((B ") . G)},{((A ") . F)}} is set

[:A,B:] . [((A ") . F),((B ") . G)] is set

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

(~ [:A,B:]) . (F,G) is set

(~ [:A,B:]) . [F,G] is set

[:A,B:] . (G,F) is set

[G,F] is V15() set

{G,F} is set

{G} is set

{{G,F},{G}} is set

[:A,B:] . [G,F] is set

A . G is set

B . F is set

[(A . G),(B . F)] is V15() set

{(A . G),(B . F)} is set

{(A . G)} is set

{{(A . G),(B . F)},{(A . G)}} is set

[(B . F),(A . G)] is V15() set

{(B . F),(A . G)} is set

{(B . F)} is set

{{(B . F),(A . G)},{(B . F)}} is set

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

proj2 [:B,A:] is set

[:B,A:] . (F,G) is set

[:B,A:] . [F,G] is set

([:B,A:] ") . ([:B,A:] . (F,G)) is set

([:B,A:] ") . ((B . F),(A . G)) is set

([:B,A:] ") . [(B . F),(A . G)] is set

(~ ([:B,A:] ")) . ((A . G),(B . F)) is set

(~ ([:B,A:] ")) . [(A . G),(B . F)] is set

A is set

B is set

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

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

id B is Relation-like B -defined B -valued Function-like one-to-one V14(B) quasi_total Element of bool [:B,B:]

[:B,B:] is Relation-like set

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

[:A,A:] is Relation-like set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) quasi_total Element of bool [:A,A:]

bool [:A,A:] is non empty set

A is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]

[:A,A:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

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

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

[:A,A:] .: (id A) is Relation-like B -defined B -valued Element of bool [:B,B:]

rng A is Element of bool B

bool B is non empty set

B is set

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

c

A . c

dom A is Element of bool A

bool A is non empty set

[c

{c

{c

{{c

[:A,A:] . (c

[:A,A:] . [c

A is Relation-like Function-like Function-yielding V37() set

B is Relation-like Function-like Function-yielding V37() set

B ** A is Relation-like Function-like Function-yielding V37() set

A is Relation-like Function-like set

A * (B ** A) is Relation-like Function-like Function-yielding V37() set

A * A is Relation-like Function-like Function-yielding V37() set

A * B is Relation-like Function-like Function-yielding V37() set

(A * B) ** (A * A) is Relation-like Function-like Function-yielding V37() set

proj1 (A * (B ** A)) is set

proj1 (B ** A) is set

A " (proj1 (B ** A)) is set

proj1 B is set

proj1 A is set

(proj1 B) /\ (proj1 A) is set

A " ((proj1 B) /\ (proj1 A)) is set

A " (proj1 A) is set

A " (proj1 B) is set

(A " (proj1 A)) /\ (A " (proj1 B)) is set

proj1 (A * B) is set

(A " (proj1 A)) /\ (proj1 (A * B)) is set

proj1 (A * A) is set

(proj1 (A * A)) /\ (proj1 (A * B)) is set

B is set

proj1 A is set

A . B is set

(A * (B ** A)) . B is Relation-like Function-like set

(B ** A) . (A . B) is Relation-like Function-like set

A . (A . B) is Relation-like Function-like set

B . (A . B) is Relation-like Function-like set

(A . (A . B)) * (B . (A . B)) is Relation-like Function-like set

(A * B) . B is Relation-like Function-like set

(A . (A . B)) * ((A * B) . B) is Relation-like Function-like set

(A * A) . B is Relation-like Function-like set

((A * A) . B) * ((A * B) . B) is Relation-like Function-like set

A is set

B is set

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

A is set

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

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

B is Relation-like [:A,B:] -defined A -valued Function-like quasi_total Element of bool [:[:A,B:],A:]

~ B is Relation-like Function-like set

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

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

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

F is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

~ F is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

A is set

B is set

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

A is set

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

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

B is Relation-like [:A,B:] -defined A -valued Function-like quasi_total Element of bool [:[:A,B:],A:]

(A,B,A,B) is Relation-like [:B,A:] -defined A -valued Function-like quasi_total Element of bool [:[:B,A:],A:]

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

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

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

rng (A,B,A,B) is Element of bool A

bool A is non empty set

rng B is Element of bool A

A is set

[:A,A:] is Relation-like set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) quasi_total Element of bool [:A,A:]

bool [:A,A:] is non empty set

B is non empty set

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

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

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

id B is Relation-like B -defined B -valued Function-like one-to-one non empty V14(B) quasi_total Element of bool [:B,B:]

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

A is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

[:A,A:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

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

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

[:A,A:] .: (id A) is Relation-like B -defined B -valued Element of bool [:B,B:]

B is set

F is set

[:A,A:] . F is set

G is set

c

[G,c

{G,c

{G} is set

{{G,c

o2 is Element of A

A . o2 is set

dom A is Element of bool A

bool A is non empty set

[:A,A:] . (o2,c

[o2,c

{o2,c

{o2} is set

{{o2,c

[:A,A:] . [o2,c

[(A . o2),(A . o2)] is V15() set

{(A . o2),(A . o2)} is set

{(A . o2)} is set

{{(A . o2),(A . o2)},{(A . o2)}} is set

A is set

[:A,A:] is Relation-like set

B is set

[:B,B:] is Relation-like set

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

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

A is set

[:A,A:] is Relation-like set

B is non empty set

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

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

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

A is Element of B

[A,A] is V15() set

{A,A} is set

{A} is set

{{A,A},{A}} is set

[:A,A:] --> [A,A] is Relation-like [:A,A:] -defined {[A,A]} -valued Function-like constant V14([:A,A:]) quasi_total Element of bool [:[:A,A:],{[A,A]}:]

{[A,A]} is Relation-like Function-like set

[:[:A,A:],{[A,A]}:] is Relation-like set

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

B is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

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

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

A --> A is Relation-like A -defined B -valued Function-like constant V14(A) quasi_total Element of bool [:A,B:]

F is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

[:F,F:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

F is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

[:F,F:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

(A,A,[:B,B:],[:F,F:]) is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

(A,A,{[A,A]},([:A,A:] --> [A,A])) is Relation-like [:A,A:] -defined {[A,A]} -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],{[A,A]}:]

A is set

[:A,A:] is Relation-like set

B is set

[:B,B:] is Relation-like set

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

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

A is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

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

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

B is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]

[:B,B:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

F is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

[:F,F:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

[:B,B:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

(A,A,[:B,B:],[:B,B:]) is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

F is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

[:F,F:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

~ [:F,F:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set

the Element of B is Element of B

[ the Element of B, the Element of B] is V15() set

{ the Element of B, the Element of B} is set

{ the Element of B} is set

{{ the Element of B, the Element of B},{ the Element of B}} is set

[:A,A:] --> [ the Element of B, the Element of B] is Relation-like [:A,A:] -defined {[ the Element of B, the Element of B]} -valued Function-like constant V14([:A,A:]) quasi_total Element of bool [:[:A,A:],{[ the Element of B, the Element of B]}:]

{[ the Element of B, the Element of B]} is Relation-like Function-like set

[:[:A,A:],{[ the Element of B, the Element of B]}:] is Relation-like set

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

F is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:B,B:]:]

A is non empty set

[:A,A:] is Relation-like non empty set

B is non empty set

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

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

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

A is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like non empty V14([:A,A:]) quasi_total (A,B) (A,B) Element of bool [:[:A,A:],[:B,B:]:]

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

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

B is Relation-like A -defined B -valued Function-like non empty V14(A) quasi_total Element of bool [:A,B:]

[:B,B:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like non empty V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

F is Relation-like A -defined B -valued Function-like non empty V14(A) quasi_total Element of bool [:A,B:]

[:F,F:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like non empty V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

(A,A,[:B,B:],[:F,F:]) is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like non empty V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

the Element of A is Element of A

B . the Element of A is Element of B

c

[c

{c

{c

{{c

[:A,A:] --> [c

{[c

[:[:A,A:],{[c

bool [:[:A,A:],{[c

dom A is Relation-like A -defined A -valued non empty Element of bool [:A,A:]

bool [:A,A:] is non empty set

o2 is set

o3 is Element of A

f is Element of A

[o3,f] is V15() set

{o3,f} is set

{o3} is set

{{o3,f},{o3}} is set

dom F is non empty Element of bool A

bool A is non empty set

dom B is non empty Element of bool A

dom [:F,F:] is Relation-like A -defined A -valued non empty Element of bool [:A,A:]

[:(dom F),(dom F):] is Relation-like A -defined A -valued non empty Element of bool [:A,A:]

[o3, the Element of A] is V15() set

{o3, the Element of A} is set

{{o3, the Element of A},{o3}} is set

B . o3 is Element of B

[c

{c

{{c

A . ( the Element of A,o3) is Element of [:B,B:]

[ the Element of A,o3] is V15() set

{ the Element of A,o3} is set

{ the Element of A} is set

{{ the Element of A,o3},{ the Element of A}} is set

A . [ the Element of A,o3] is set

[:F,F:] . (o3, the Element of A) is Element of [:B,B:]

[:F,F:] . [o3, the Element of A] is set

F . o3 is Element of B

F . the Element of A is Element of B

[(F . o3),(F . the Element of A)] is V15() set

{(F . o3),(F . the Element of A)} is set

{(F . o3)} is set

{{(F . o3),(F . the Element of A)},{(F . o3)}} is set

[f, the Element of A] is V15() set

{f, the Element of A} is set

{f} is set

{{f, the Element of A},{f}} is set

B . f is Element of B

[c

{c

{{c

A . ( the Element of A,f) is Element of [:B,B:]

[ the Element of A,f] is V15() set

{ the Element of A,f} is set

{{ the Element of A,f},{ the Element of A}} is set

A . [ the Element of A,f] is set

[:F,F:] . (f, the Element of A) is Element of [:B,B:]

[:F,F:] . [f, the Element of A] is set

F . f is Element of B

[(F . f),(F . the Element of A)] is V15() set

{(F . f),(F . the Element of A)} is set

{(F . f)} is set

{{(F . f),(F . the Element of A)},{(F . f)}} is set

[f,o3] is V15() set

{f,o3} is set

{{f,o3},{f}} is set

A . o2 is set

[:B,B:] . (o3,f) is Element of [:B,B:]

[:B,B:] . [o3,f] is set

[:F,F:] . (f,o3) is Element of [:B,B:]

[:F,F:] . [f,o3] is set

A is set

B is set

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

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

A is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]

F is Relation-like B -defined Function-like V14(B) set

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

[[0]] A is Relation-like empty-yielding A -defined Function-like V14(A) Function-yielding V37() set

A --> {} is Relation-like A -defined {{}} -valued Function-like constant V14(A) quasi_total Element of bool [:A,{{}}:]

{{}} is set

[:A,{{}}:] is Relation-like set

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

G is non empty set

[:A,G:] is Relation-like set

bool [:A,G:] is non empty set

c

o2 is Relation-like G -defined Function-like non empty V14(G) set

c

the Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of B,c

f is Relation-like A -defined Function-like V14(A) set

K is non empty set

[:A,K:] is Relation-like set

bool [:A,K:] is non empty set

g9 is Relation-like K -defined Function-like non empty V14(K) set

f9 is Relation-like A -defined K -valued Function-like V14(A) quasi_total Element of bool [:A,K:]

f99 is Relation-like A -defined K -valued Function-like V14(A) quasi_total Element of bool [:A,K:]

g99 is Relation-like K -defined Function-like non empty V14(K) set

g is Relation-like A -defined Function-like V14(A) set

f99 * g99 is Relation-like A -defined Function-like V14(A) set

A is set

B is non empty set

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

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

A is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

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

F is Relation-like B -defined Function-like non empty V14(B) set

A * F is Relation-like A -defined Function-like V14(A) set

G is Relation-like A -defined Function-like V14(A) set

c

[:A,c

bool [:A,c

o3 is Relation-like A -defined c

o2 is Relation-like c

o3 * o2 is Relation-like A -defined Function-like V14(A) set

A is set

B is set

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

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

A is Relation-like A -defined B -valued Function-like quasi_total Element of bool [:A,B:]

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

F is Relation-like B -defined Function-like V14(B) set

G is Relation-like A -defined Function-like V14(A) (A,B,A,B,F)

c

[:A,c

bool [:A,c

o3 is Relation-like A -defined c

o2 is Relation-like c

o3 * o2 is Relation-like A -defined Function-like V14(A) set

[[0]] A is Relation-like empty-yielding A -defined Function-like V14(A) Function-yielding V37() set

A --> {} is Relation-like A -defined {{}} -valued Function-like constant V14(A) quasi_total Element of bool [:A,{{}}:]

[:A,{{}}:] is Relation-like set

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

A is set

B is non empty set

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

bool [:A,B:] 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 is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

F is Relation-like B -defined A -valued Function-like non empty V14(B) quasi_total Element of bool [:B,A:]

F * B is Relation-like A -defined A -valued Function-like V14(A) quasi_total Element of bool [:A,A:]

[:A,A:] is Relation-like set

bool [:A,A:] is non empty set

G is Relation-like B -defined Function-like non empty V14(B) set

B * G is Relation-like A -defined Function-like V14(A) set

c

o2 is Relation-like B -defined Function-like non empty V14(B) Function-yielding V37() (B,A,F,G,c

B * o2 is Relation-like A -defined Function-like V14(A) Function-yielding V37() set

(F * B) * c

F * c

B * (F * c

A is set

B is non empty set

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

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

[:A,A:] is Relation-like set

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

A is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

[:A,A:] is Relation-like [:A,A:] -defined [:B,B:] -valued Function-like V14([:A,A:]) quasi_total Element of bool [:[:A,A:],[:B,B:]:]

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

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

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

F is Relation-like [:B,B:] -defined Function-like non empty V14([:B,B:]) set

G is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) Function-yielding V37() ([:A,A:],[:B,B:],[:A,A:],B,F)

~ G is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) Function-yielding V37() set

~ B is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

~ F is Relation-like [:B,B:] -defined Function-like non empty V14([:B,B:]) set

[:A,A:] * F is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

c

~ c

~ ([:A,A:] * F) is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

[:A,A:] * (~ F) is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

A is non empty set

B is non empty set

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

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

A is Relation-like A -defined Function-like non empty V14(A) set

B is Relation-like B -defined Function-like non empty V14(B) set

F is Element of B

B . F is set

A --> F is Relation-like A -defined B -valued Function-like constant non empty V14(A) quasi_total Element of bool [:A,B:]

G is Element of B . F

{ [b

c

{G} is set

{ [b

o2 is Relation-like Function-like set

proj1 o2 is set

{ b

o3 is Relation-like A -defined Function-like non empty V14(A) set

{ [b

f is set

g is Element of A

dom c

bool A is non empty set

c

B . (c

c

(c

o3 . g is set

A . g is set

(A . g) --> G is Relation-like A . g -defined {G} -valued Function-like constant V14(A . g) quasi_total Element of bool [:(A . g),{G}:]

[:(A . g),{G}:] is Relation-like set

bool [:(A . g),{G}:] is non empty set

o3 . f is set

A . f is set

[:(A . f),((c

bool [:(A . f),((c

A is set

B is non empty set

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

bool [:A,B:] 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 is Relation-like A -defined B -valued Function-like V14(A) quasi_total Element of bool [:A,B:]

F is Relation-like B -defined A -valued Function-like non empty V14(B) quasi_total Element of bool [:B,A:]

F * B is Relation-like A -defined A -valued Function-like V14(A) quasi_total Element of bool [:A,A:]

[:A,A:] is Relation-like set

bool [:A,A:] is non empty set

G is Relation-like A -defined Function-like V14(A) set

c

B * c

o2 is Relation-like A -defined Function-like non empty V14(A) set

(F * B) * o2 is Relation-like A -defined Function-like V14(A) set

o3 is Relation-like A -defined Function-like V14(A) Function-yielding V37() (A,B,B,G,c

f is Relation-like A -defined Function-like V14(A) Function-yielding V37() (A,A,F * B,B * c

f ** o3 is Relation-like A -defined Function-like V14(A) Function-yielding V37() set

g is Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of B * c

dom g is Element of bool A

bool A is non empty set

K is Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of G,B * c

dom K is Element of bool A

g ** K is Relation-like A -defined Function-like V14(A) Function-yielding V37() set

dom (g ** K) is Element of bool A

(dom g) /\ (dom K) is Element of bool A

f9 is Relation-like A -defined Function-like V14(A) set

g9 is set

f9 . g9 is set

G . g9 is set

((F * B) * o2) . g9 is set

[:(G . g9),(((F * B) * o2) . g9):] is Relation-like set

bool [:(G . g9),(((F * B) * o2) . g9):] is non empty set

(B * c

[:(G . g9),((B * c

bool [:(G . g9),((B * c

K . g9 is Relation-like Function-like set

[:((B * c

bool [:((B * c

g . g9 is Relation-like Function-like set

g99 is Relation-like G . g9 -defined (B * c

f99 is Relation-like (B * c

f99 * g99 is Relation-like G . g9 -defined ((F * B) * o2) . g9 -valued Function-like Element of bool [:(G . g9),(((F * B) * o2) . g9):]

A is non empty AltGraph

B is non empty AltGraph

the carrier of A is non empty set

the carrier of B is non empty set

[: the carrier of B, the carrier of B:] is Relation-like non empty set

A is (A,B)

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

[: the carrier of A, the carrier of A:] is Relation-like non empty set

[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set

bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set

B is Element of the carrier of A

the of A . (B,B) is Element of [: the carrier of B, the carrier of B:]

[B,B] is V15() set

{B,B} is set

{B} is set

{{B,B},{B}} is set

the of A . [B,B] is set

( the of A . (B,B)) `1 is set

A is 1-sorted

B is 1-sorted

A is non empty AltGraph

B is non empty AltGraph

A is (A,B)

the carrier of A is non empty set

the carrier of B is non empty set

[: the carrier of B, the carrier of B:] is Relation-like non empty set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

[: the carrier of A, the carrier of A:] is Relation-like non empty set

[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set

bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set

id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one non empty V14( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of A:]

bool [: the carrier of A, the carrier of A:] is non empty set

the of A .: (id the carrier of A) is Relation-like the carrier of B -defined the carrier of B -valued Element of bool [: the carrier of B, the carrier of B:]

bool [: the carrier of B, the carrier of B:] is non empty set

id the carrier of B is Relation-like the carrier of B -defined the carrier of B -valued Function-like one-to-one non empty V14( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of B:]

B is Element of the carrier of A

[B,B] is V15() set

{B,B} is set

{B} is set

{{B,B},{B}} is set

the of A . (B,B) is Element of [: the carrier of B, the carrier of B:]

the of A . [B,B] is set

F is set

G is set

[F,G] is V15() set

{F,G} is set

{F} is set

{{F,G},{F}} is set

(A,B,A,B) is Element of the carrier of B

( the of A . (B,B)) `1 is set

[(A,B,A,B),(A,B,A,B)] is V15() set

{(A,B,A,B),(A,B,A,B)} is set

{(A,B,A,B)} is set

{{(A,B,A,B),(A,B,A,B)},{(A,B,A,B)}} is set

B is set

F is set

the of A . F is set

G is Element of the carrier of A

c

[G,c

{G,c

{G} is set

{{G,c

o2 is Element of the carrier of A

(A,B,A,o2) is Element of the carrier of B

the of A . (o2,o2) is Element of [: the carrier of B, the carrier of B:]

[o2,o2] is V15() set

{o2,o2} is set

{o2} is set

{{o2,o2},{o2}} is set

the of A . [o2,o2] is set

( the of A . (o2,o2)) `1 is set

[(A,B,A,o2),(A,B,A,o2)] is V15() set

{(A,B,A,o2),(A,B,A,o2)} is set

{(A,B,A,o2)} is set

{{(A,B,A,o2),(A,B,A,o2)},{(A,B,A,o2)}} is set

A is non empty reflexive AltGraph

B is non empty reflexive AltGraph

the carrier of B is non empty set

the carrier of A is non empty set

A is (A,B)

id the carrier of B is Relation-like the carrier of B -defined the carrier of B -valued Function-like one-to-one non empty V14( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of B:]

[: the carrier of B, the carrier of B:] is Relation-like non empty set

bool [: the carrier of B, the carrier of B:] is non empty set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like non empty V14([: the carrier of A, the carrier of A:]) quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like non empty set

bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set

id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one non empty V14( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of A:]

bool [: the carrier of A, the carrier of A:] is non empty set

the of A .: (id the carrier of A) is Relation-like the carrier of B -defined the carrier of B -valued Element of bool [: the carrier of B, the carrier of B:]

B is Element of the carrier of B

[B,B] is V15() set

{B,B} is set

{B} is set

{{B,B},{B}} is set

F is Element of [: the carrier of B, the carrier of B:]

G is Element of [: the carrier of A, the carrier of A:]

the of A . G is Element of [: the carrier of B, the carrier of B:]

c

o2 is set

[c

{c

{c

{{c

o3 is Element of the carrier of A

(A,B,A,o3) is Element of the carrier of B

the of A . (o3,o3) is Element of [: the carrier of B, the carrier of B:]

[o3,o3] is V15() set

{o3,o3} is set

{o3} is set

{{o3,o3},{o3}} is set

the of A . [o3,o3] is set

( the of A . (o3,o3)) `1 is set

A is non empty AltGraph

B is non empty AltGraph

A is 1-sorted

B is 1-sorted

A is AltGraph

B is AltGraph

the carrier of A is set

[: the carrier of A, the carrier of A:] is Relation-like set

the carrier of B is set

[: the carrier of B, the carrier of B:] is Relation-like set

[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like set

bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set

the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V14([: the carrier of B, the carrier of B:]) set

the Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) Function-yielding V37() ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:], the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:], the Arrows of A, the Arrows of B) is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) Function-yielding V37() ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:], the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:], the Arrows of A, the Arrows of B)

(A,B, the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:], the Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) Function-yielding V37() ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:], the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:], the Arrows of A, the Arrows of B)) is (A,B) (A,B)

F is (A,B) (A,B)

the of F is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

the carrier of A is set

[: the carrier of A, the carrier of A:] is Relation-like set

the carrier of B is set

[: the carrier of B, the carrier of B:] is Relation-like set

[:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like set

bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is non empty set

the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:] is Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of bool [:[: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]:]

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

the Arrows of B is Relation-like [: the carrier of B, the carrier of B:] -defined Function-like V14([: the carrier of B, the carrier of B:]) set

the Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) Function-yielding V37() ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:], the Relation-like [: the carrier of A, the carrier of A:] -defined [: the carrier of B, the carrier of B:] -valued Function-like quasi_total ( the carrier of A, the carrier of B) Element of