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
F1() is non empty set
F2() is Relation-like Function-like set
{ [[b1,b2],F5(b1,b2)] where b1, b2 is Element of F1() : P1[b1,b2] } is set
F3() is Element of F1()
F4() is Element of F1()
F2() . (F3(),F4()) is set
[F3(),F4()] is V15() set
{F3(),F4()} is set
{F3()} is set
{{F3(),F4()},{F3()}} is set
F2() . [F3(),F4()] is set
F5(F3(),F4()) is set
[:F1(),F1():] is Relation-like non empty set
{ [b1,H1(b1)] where b1 is Element of [:F1(),F1():] : S1[b1] } is set
{ [b1,F5((b1 `1),(b1 `2))] where b1 is Element of [:F1(),F1():] : P1[b1 `1 ,b1 `2 ] } is set
A is set
B is Element of F1()
A is Element of F1()
[B,A] is V15() set
{B,A} is set
{B} is set
{{B,A},{B}} is set
F5(B,A) is set
[[B,A],F5(B,A)] is V15() set
{[B,A],F5(B,A)} is set
{[B,A]} is Relation-like Function-like set
{{[B,A],F5(B,A)},{[B,A]}} is set
B is Element of [:F1(),F1():]
B `1 is set
B `2 is set
A is set
B is Element of [:F1(),F1():]
B `1 is set
B `2 is set
F5((B `1),(B `2)) is set
[B,F5((B `1),(B `2))] is V15() set
{B,F5((B `1),(B `2))} is set
{B} is set
{{B,F5((B `1),(B `2))},{B}} is set
A is Element of F1()
B is Element of F1()
[A,B] is V15() set
{A,B} is set
{A} is set
{{A,B},{A}} is set
A is Element of [:F1(),F1():]
A `1 is set
A `2 is set
F2() . A is set
F5((A `1),(A `2)) is set
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
c7 is set
[o2,c7] is V15() set
{o2,c7} is set
{o2} is set
{{o2,c7},{o2}} is set
[c7,o2] is V15() set
{c7,o2} is set
{c7} is set
{{c7,o2},{c7}} is set
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
c7 is set
[G,c7] is V15() set
{G,c7} is set
{G} is set
{{G,c7},{G}} is set
o2 is set
o3 is set
[o2,o3] is V15() set
{o2,o3} is set
{o2} is set
{{o2,o3},{o2}} is set
[c7,G] is V15() set
{c7,G} is set
{c7} is set
{{c7,G},{c7}} is set
proj1 A is set
[o3,o2] is V15() set
{o3,o2} is set
{o3} is set
{{o3,o2},{o3}} is set
A . (c7,G) is set
A . [c7,G] is set
(~ A) . (G,c7) is set
(~ A) . [G,c7] is set
(~ 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
c7 is set
o2 is set
[c7,o2] is V15() set
{c7,o2} is set
{c7} is set
{{c7,o2},{c7}} is set
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:] . (c7,o2) is set
[:B,A:] . [c7,o2] is set
B . c7 is set
A . o2 is set
[(B . c7),(A . o2)] is V15() set
{(B . c7),(A . o2)} is set
{(B . c7)} is set
{{(B . c7),(A . o2)},{(B . c7)}} 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 . o2),(B . c7)] is V15() set
{(A . o2),(B . c7)} is set
{(A . o2)} is set
{{(A . o2),(B . c7)},{(A . o2)}} is set
[:A,B:] . (o2,c7) is set
[o2,c7] is V15() set
{o2,c7} is set
{o2} is set
{{o2,c7},{o2}} is set
[:A,B:] . [o2,c7] is set
(~ [:A,B:]) . (c7,o2) is set
(~ [:A,B:]) . [c7,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
(~ [: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
c7 is set
A . c7 is set
dom A is Element of bool A
bool A is non empty set
[c7,c7] is V15() set
{c7,c7} is set
{c7} is set
{{c7,c7},{c7}} is set
[:A,A:] . (c7,c7) is set
[:A,A:] . [c7,c7] is set
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
c7 is set
[G,c7] is V15() set
{G,c7} is set
{G} is set
{{G,c7},{G}} is set
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,c7) is set
[o2,c7] is V15() set
{o2,c7} is set
{o2} is set
{{o2,c7},{o2}} is set
[:A,A:] . [o2,c7] is set
[(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
c7 is Element of B
[c7,c7] is V15() set
{c7,c7} is set
{c7} is set
{{c7,c7},{c7}} is set
[:A,A:] --> [c7,c7] is Relation-like [:A,A:] -defined {[c7,c7]} -valued Function-like constant non empty V14([:A,A:]) quasi_total Element of bool [:[:A,A:],{[c7,c7]}:]
{[c7,c7]} is Relation-like Function-like set
[:[:A,A:],{[c7,c7]}:] is Relation-like set
bool [:[:A,A:],{[c7,c7]}:] is non empty set
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
[c7,(B . o3)] is V15() set
{c7,(B . o3)} is set
{{c7,(B . o3)},{c7}} is set
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
[c7,(B . f)] is V15() set
{c7,(B . f)} is set
{{c7,(B . f)},{c7}} is set
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
c7 is Relation-like A -defined G -valued Function-like V14(A) quasi_total Element of bool [:A,G:]
o2 is Relation-like G -defined Function-like non empty V14(G) set
c7 * o2 is Relation-like A -defined Function-like V14(A) set
the Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of B,c7 * o2 is Relation-like A -defined Function-like V14(A) Function-yielding V37() ManySortedFunction of B,c7 * o2
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
c7 is non empty set
[:A,c7:] is Relation-like set
bool [:A,c7:] is non empty set
o3 is Relation-like A -defined c7 -valued Function-like V14(A) quasi_total Element of bool [:A,c7:]
o2 is Relation-like c7 -defined Function-like non empty V14(c7) set
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)
c7 is non empty set
[:A,c7:] is Relation-like set
bool [:A,c7:] is non empty set
o3 is Relation-like A -defined c7 -valued Function-like V14(A) quasi_total Element of bool [:A,c7:]
o2 is Relation-like c7 -defined Function-like non empty V14(c7) set
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
c7 is Relation-like A -defined Function-like non empty V14(A) set
o2 is Relation-like B -defined Function-like non empty V14(B) Function-yielding V37() (B,A,F,G,c7)
B * o2 is Relation-like A -defined Function-like V14(A) Function-yielding V37() set
(F * B) * c7 is Relation-like A -defined Function-like V14(A) set
F * c7 is Relation-like B -defined Function-like non empty V14(B) set
B * (F * c7) 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,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
c7 is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) Function-yielding V37() ManySortedFunction of B,[:A,A:] * F
~ c7 is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) Function-yielding V37() ManySortedFunction of ~ B, ~ ([:A,A:] * F)
~ ([: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
{ [b1,((A . b1) --> G)] where b1 is Element of A : verum } is set
c7 is Relation-like A -defined B -valued Function-like non empty V14(A) quasi_total Element of bool [:A,B:]
{G} is set
{ [b1,H1(b1)] where b1 is Element of A : S1[b1] } is set
o2 is Relation-like Function-like set
proj1 o2 is set
{ b1 where b1 is Element of A : S1[b1] } is set
o3 is Relation-like A -defined Function-like non empty V14(A) set
{ [b1,H2(b1)] where b1 is Element of A : S1[b1] } is set
f is set
g is Element of A
dom c7 is non empty Element of bool A
bool A is non empty set
c7 . f is set
B . (c7 . f) is set
c7 * B is Relation-like A -defined Function-like non empty V14(A) set
(c7 * B) . f is set
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),((c7 * B) . f):] is Relation-like set
bool [:(A . f),((c7 * B) . f):] 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 A -defined Function-like V14(A) set
c7 is Relation-like B -defined Function-like non empty V14(B) set
B * c7 is Relation-like A -defined Function-like V14(A) set
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,c7)
f is Relation-like A -defined Function-like V14(A) Function-yielding V37() (A,A,F * B,B * c7,o2)
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 * c7,(F * B) * o2
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 * c7
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 * c7) . g9 is set
[:(G . g9),((B * c7) . g9):] is Relation-like set
bool [:(G . g9),((B * c7) . g9):] is non empty set
K . g9 is Relation-like Function-like set
[:((B * c7) . g9),(((F * B) * o2) . g9):] is Relation-like set
bool [:((B * c7) . g9),(((F * B) * o2) . g9):] is non empty set
g . g9 is Relation-like Function-like set
g99 is Relation-like G . g9 -defined (B * c7) . g9 -valued Function-like quasi_total Element of bool [:(G . g9),((B * c7) . g9):]
f99 is Relation-like (B * c7) . g9 -defined ((F * B) * o2) . g9 -valued Function-like quasi_total Element of bool [:((B * c7) . g9),(((F * B) * o2) . g9):]
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
c7 is Element of the carrier of A
[G,c7] is V15() set
{G,c7} is set
{G} is set
{{G,c7},{G}} is set
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:]
c7 is set
o2 is set
[c7,o2] is V15() set
{c7,o2} is set
{c7} is set
{{c7,o2},{c7}} is set
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