K168() is Element of bool K164()
K164() is set
bool K164() is non empty set
K116() is set
bool K116() is non empty set
{} is Function-like functional empty set
the Function-like functional empty set is Function-like functional empty set
1 is non empty set
{{},1} is non empty set
bool K168() is non empty set
id {} is Relation-like V6() V8() V9() V13() Function-like one-to-one set
the non empty set is non empty set
[: the non empty set , the non empty set :] is non empty set
bool [: the non empty set , the non empty set :] is non empty set
id the non empty set is Relation-like the non empty set -defined the non empty set -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the non empty set ) quasi_total onto bijective Element of bool [: the non empty set , the non empty set :]
o1 is Relation-like the non empty set -defined the non empty set -valued Element of bool [: the non empty set , the non empty set :]
o2 is Relation-like the non empty set -defined the non empty set -valued V6() V9() V13() V24( the non empty set ) quasi_total Element of bool [: the non empty set , the non empty set :]
RelStr(# the non empty set ,o2 #) is non empty strict V65() reflexive transitive antisymmetric RelStr
id {} is Relation-like {} -defined {} -valued V6() V8() V9() V13() Function-like one-to-one constant functional empty V24( {} ) quasi_total onto bijective Element of bool [:{},{}:]
[:{},{}:] is set
bool [:{},{}:] is non empty set
RelStr(# {},(id {}) #) is strict V65() reflexive transitive antisymmetric RelStr
P is empty trivial V56() V61( {} ) RelStr
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Function-like one-to-one constant functional empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
the carrier of P is Function-like functional empty trivial V41() set
[: the carrier of P, the carrier of P:] is set
bool [: the carrier of P, the carrier of P:] is non empty set
P is RelStr
the carrier of P is set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is set
bool [: the carrier of P, the carrier of P:] is non empty set
P is RelStr
P is RelStr
the carrier of P is set
bool the carrier of P is non empty set
P is RelStr
the carrier of P is set
bool the carrier of P is non empty set
P is non empty () RelStr
the carrier of P is non empty set
o1 is Element of the carrier of P
o2 is Element of the carrier of P
[o1,o2] is V25() Element of [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
{o1,o2} is non empty set
{o1} is non empty set
{{o1,o2},{o1}} is non empty set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
bool [: the carrier of P, the carrier of P:] is non empty set
id the carrier of P is Relation-like the carrier of P -defined the carrier of P -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of P) quasi_total onto bijective Element of bool [: the carrier of P, the carrier of P:]
P is Relation-like set
o1 is set
{o1} is non empty set
[:{o1},{o1}:] is non empty set
bool [:{o1},{o1}:] is non empty set
id {o1} is Relation-like {o1} -defined {o1} -valued V6() V8() V9() V13() Function-like one-to-one non empty V24({o1}) quasi_total onto bijective Element of bool [:{o1},{o1}:]
[o1,o1] is V25() set
{o1,o1} is non empty set
{{o1,o1},{o1}} is non empty set
{[o1,o1]} is Function-like non empty set
P is non empty RelStr
the carrier of P is non empty set
[#] P is non empty non proper Element of bool the carrier of P
bool the carrier of P is non empty set
o1 is Element of the carrier of P
{o1} is non empty Element of bool the carrier of P
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
id {o1} is Relation-like {o1} -defined {o1} -valued V6() V8() V9() V13() Function-like one-to-one non empty V24({o1}) quasi_total onto bijective Element of bool [:{o1},{o1}:]
[:{o1},{o1}:] is non empty set
bool [:{o1},{o1}:] is non empty set
[o1,o1] is V25() Element of [: the carrier of P, the carrier of P:]
{o1,o1} is non empty set
{o1} is non empty set
{{o1,o1},{o1}} is non empty set
{[o1,o1]} is Relation-like the carrier of P -defined the carrier of P -valued Function-like non empty Element of bool [: the carrier of P, the carrier of P:]
[:{o1},{o1}:] is Relation-like the carrier of P -defined the carrier of P -valued non empty Element of bool [: the carrier of P, the carrier of P:]
A is set
P is non empty RelStr
[#] P is non empty non proper Element of bool the carrier of P
the carrier of P is non empty set
bool the carrier of P is non empty set
o1 is set
{o1} is non empty set
o2 is non empty set
bool o2 is non empty set
A is non empty Element of bool o2
B is non empty Element of bool o2
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
A is Element of bool the carrier of P
B is Element of bool the carrier of P
A \/ B is Element of bool the carrier of P
the InternalRel of P |_2 A is Relation-like set
the InternalRel of P |_2 B is Relation-like set
( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) is set
P is non empty V65() reflexive transitive antisymmetric () RelStr
the carrier of P is non empty set
o1 is Element of the carrier of P
o2 is Element of the carrier of P
{o1} is non empty Element of bool the carrier of P
bool the carrier of P is non empty set
the carrier of P \ {o1} is Element of bool the carrier of P
( the carrier of P \ {o1}) \/ {o1} is non empty Element of bool the carrier of P
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued V6() V9() V13() V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
A is non empty Element of bool the carrier of P
[:A,A:] is Relation-like the carrier of P -defined the carrier of P -valued non empty Element of bool [: the carrier of P, the carrier of P:]
B is non empty Element of bool the carrier of P
[:B,B:] is Relation-like the carrier of P -defined the carrier of P -valued non empty Element of bool [: the carrier of P, the carrier of P:]
[:A,A:] \/ [:B,B:] is Relation-like the carrier of P -defined the carrier of P -valued non empty Element of bool [: the carrier of P, the carrier of P:]
x is set
e is set
j is set
[e,j] is V25() set
{e,j} is non empty set
{e} is non empty set
{{e,j},{e}} is non empty set
id the carrier of P is Relation-like the carrier of P -defined the carrier of P -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of P) quasi_total onto bijective Element of bool [: the carrier of P, the carrier of P:]
[e,e] is V25() set
{e,e} is non empty set
{{e,e},{e}} is non empty set
the carrier of P \ A is Element of bool the carrier of P
the carrier of P /\ B is Element of bool the carrier of P
[e,e] is V25() set
{e,e} is non empty set
{{e,e},{e}} is non empty set
the InternalRel of P /\ ([:A,A:] \/ [:B,B:]) is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
the InternalRel of P |_2 A is Relation-like set
the InternalRel of P /\ [:A,A:] is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
the InternalRel of P |_2 B is Relation-like set
the InternalRel of P /\ [:B,B:] is Relation-like the carrier of P -defined the carrier of P -valued Element of bool [: the carrier of P, the carrier of P:]
( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) is set
[#] P is non empty non proper Element of bool the carrier of P
the set is set
{ the set } is non empty set
id { the set } is Relation-like { the set } -defined { the set } -valued V6() V8() V9() V13() Function-like one-to-one non empty V24({ the set }) quasi_total onto bijective Element of bool [:{ the set },{ the set }:]
[:{ the set },{ the set }:] is non empty set
bool [:{ the set },{ the set }:] is non empty set
RelStr(# { the set },(id { the set }) #) is non empty strict V65() reflexive transitive antisymmetric RelStr
o1 is non empty V65() reflexive transitive antisymmetric RelStr
[#] o1 is non empty non proper Element of bool the carrier of o1
the carrier of o1 is non empty set
bool the carrier of o1 is non empty set
2 is non empty set
{1,2} is non empty set
id {1,2} is Relation-like {1,2} -defined {1,2} -valued V6() V8() V9() V13() Function-like one-to-one non empty V24({1,2}) quasi_total onto bijective Element of bool [:{1,2},{1,2}:]
[:{1,2},{1,2}:] is non empty set
bool [:{1,2},{1,2}:] is non empty set
RelStr(# {1,2},(id {1,2}) #) is non empty strict V65() reflexive transitive antisymmetric RelStr
P is non empty V65() reflexive transitive antisymmetric RelStr
o1 is non empty V65() reflexive transitive antisymmetric () RelStr
the carrier of o1 is non empty set
B is Element of the carrier of o1
x is Element of the carrier of o1
o2 is Element of the carrier of o1
A is Element of the carrier of o1
P is non empty V65() reflexive transitive antisymmetric RelStr
the non empty V65() reflexive transitive antisymmetric RelStr is non empty V65() reflexive transitive antisymmetric RelStr
{ the non empty V65() reflexive transitive antisymmetric RelStr } is non empty set
o2 is set
P is non empty () set
o1 is Element of P
P is RelStr
the carrier of P is set
o1 is RelStr
the carrier of o1 is set
[: the carrier of P, the carrier of o1:] is set
bool [: the carrier of P, the carrier of o1:] is non empty set
P is non empty RelStr
the carrier of P is non empty set
o1 is non empty RelStr
the carrier of o1 is non empty set
[: the carrier of P, the carrier of o1:] is non empty set
bool [: the carrier of P, the carrier of o1:] is non empty set
o2 is non empty RelStr
the carrier of o2 is non empty set
[: the carrier of o1, the carrier of o2:] is non empty set
bool [: the carrier of o1, the carrier of o2:] is non empty set
[: the carrier of P, the carrier of o2:] is non empty set
bool [: the carrier of P, the carrier of o2:] is non empty set
A is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o1:]
B is Relation-like the carrier of o1 -defined the carrier of o2 -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of o2:]
B * A is Relation-like the carrier of P -defined the carrier of o2 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o2:]
x is Relation-like the carrier of P -defined the carrier of o2 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o2:]
e is Element of the carrier of P
A . e is Element of the carrier of o1
j is Element of the carrier of P
A . j is Element of the carrier of o1
dom A is Element of bool the carrier of P
bool the carrier of P is non empty set
B . (A . e) is Element of the carrier of o2
(B * A) . e is Element of the carrier of o2
B . (A . j) is Element of the carrier of o2
(B * A) . j is Element of the carrier of o2
f is Element of the carrier of o1
j9 is Element of the carrier of o1
f9 is Element of the carrier of o2
x . e is Element of the carrier of o2
e9 is Element of the carrier of o2
x . j is Element of the carrier of o2
P is non empty RelStr
id P is Relation-like the carrier of P -defined the carrier of P -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
the carrier of P is non empty set
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
id the carrier of P is Relation-like the carrier of P -defined the carrier of P -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of P) quasi_total onto bijective Element of bool [: the carrier of P, the carrier of P:]
o2 is Element of the carrier of P
A is Element of the carrier of P
(id P) . o2 is set
(id P) . A is set
B is Element of the carrier of P
x is Element of the carrier of P
e is Element of the carrier of P
(id P) . e is Element of the carrier of P
(id P) . o2 is Element of the carrier of P
(id P) . A is Element of the carrier of P
P is RelStr
the carrier of P is set
o1 is RelStr
the carrier of o1 is set
[: the carrier of P, the carrier of o1:] is set
bool [: the carrier of P, the carrier of o1:] is non empty set
Funcs ( the carrier of P, the carrier of o1) is functional set
o2 is set
A is set
B is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
x is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
B is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
o2 is set
A is set
B is set
x is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
B is set
x is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
P is non empty RelStr
o1 is non empty RelStr
(P,o1) is set
o2 is non empty RelStr
(o1,o2) is set
(P,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
the carrier of P is non empty set
the carrier of o1 is non empty set
[: the carrier of P, the carrier of o1:] is non empty set
bool [: the carrier of P, the carrier of o1:] is non empty set
Funcs ( the carrier of P, the carrier of o1) is functional non empty FUNCTION_DOMAIN of the carrier of P, the carrier of o1
x is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o1:]
the carrier of o2 is non empty set
[: the carrier of o1, the carrier of o2:] is non empty set
bool [: the carrier of o1, the carrier of o2:] is non empty set
Funcs ( the carrier of o1, the carrier of o2) is functional non empty FUNCTION_DOMAIN of the carrier of o1, the carrier of o2
e is Relation-like the carrier of o1 -defined the carrier of o2 -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of o2:]
[: the carrier of P, the carrier of o2:] is non empty set
bool [: the carrier of P, the carrier of o2:] is non empty set
e * x is Relation-like the carrier of P -defined the carrier of o2 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o2:]
j is Relation-like the carrier of P -defined the carrier of o2 -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of o2:]
Funcs ( the carrier of P, the carrier of o2) is functional non empty FUNCTION_DOMAIN of the carrier of P, the carrier of o2
P is non empty RelStr
the carrier of P is non empty set
id the carrier of P is Relation-like the carrier of P -defined the carrier of P -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of P) quasi_total onto bijective Element of bool [: the carrier of P, the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty set
bool [: the carrier of P, the carrier of P:] is non empty set
(P,P) is set
id P is Relation-like the carrier of P -defined the carrier of P -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
o1 is Relation-like the carrier of P -defined the carrier of P -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
o2 is Relation-like the carrier of P -defined the carrier of P -valued Function-like non empty V24( the carrier of P) quasi_total Element of bool [: the carrier of P, the carrier of P:]
Funcs ( the carrier of P, the carrier of P) is functional non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
P is non empty RelStr
(P,P) is set
P is set
B is 1-sorted
o1 is set
o2 is set
the carrier of B is set
x is 1-sorted
A is set
the carrier of x is set
o1 is set
o2 is set
A is set
B is 1-sorted
the carrier of B is set
B is 1-sorted
the carrier of B is set
x is 1-sorted
the carrier of x is set
A is 1-sorted
the carrier of A is set
A is 1-sorted
the carrier of A is set
B is 1-sorted
the carrier of B is set
o1 is set
o2 is set
A is set
B is 1-sorted
the carrier of B is set
B is 1-sorted
the carrier of B is set
P is non empty () set
o1 is non empty V65() reflexive transitive antisymmetric (P)
the carrier of o1 is non empty set
(P) is set
P is non empty () set
(P) is set
P is 1-sorted
{P} is non empty set
({P}) is set
the carrier of P is set
{ the carrier of P} is non empty set
o1 is set
o2 is 1-sorted
the carrier of o2 is set
o1 is set
P is 1-sorted
o1 is 1-sorted
{P,o1} is non empty set
({P,o1}) is set
the carrier of P is set
the carrier of o1 is set
{ the carrier of P, the carrier of o1} is non empty set
o2 is set
A is 1-sorted
the carrier of A is set
o2 is set
P is non empty () set
(P) is non empty set
Funcs (P) is functional non empty set
o1 is non empty V65() reflexive transitive antisymmetric (P)
o2 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o2) is set
the carrier of o1 is non empty set
the carrier of o2 is non empty set
x is set
[: the carrier of o1, the carrier of o2:] is non empty set
bool [: the carrier of o1, the carrier of o2:] is non empty set
Funcs ( the carrier of o1, the carrier of o2) is functional non empty FUNCTION_DOMAIN of the carrier of o1, the carrier of o2
A is Element of (P)
B is Element of (P)
Funcs (A,B) is functional set
e is Relation-like the carrier of o1 -defined the carrier of o2 -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of o2:]
P is RelStr
o1 is RelStr
(P,o1) is set
the carrier of P is set
the carrier of o1 is set
Funcs ( the carrier of P, the carrier of o1) is functional set
o2 is set
[: the carrier of P, the carrier of o1:] is set
bool [: the carrier of P, the carrier of o1:] is non empty set
A is Relation-like the carrier of P -defined the carrier of o1 -valued Function-like quasi_total Element of bool [: the carrier of P, the carrier of o1:]
P is non empty V65() reflexive transitive antisymmetric RelStr
o1 is non empty V65() reflexive transitive antisymmetric RelStr
(P,o1) is set
the carrier of P is non empty set
the carrier of o1 is non empty set
Funcs ( the carrier of P, the carrier of o1) is functional non empty FUNCTION_DOMAIN of the carrier of P, the carrier of o1
bool (Funcs ( the carrier of P, the carrier of o1)) is non empty set
o2 is functional Element of bool (Funcs ( the carrier of P, the carrier of o1))
P is non empty () set
(P) is non empty set
Funcs (P) is functional non empty set
[:P,P:] is non empty set
o1 is non empty V65() reflexive transitive antisymmetric (P)
o2 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o2) is functional set
A is non empty V65() reflexive transitive antisymmetric (P)
(o2,A) is functional set
(o1,A) is functional set
B is Relation-like Function-like Element of Funcs (P)
x is Relation-like Function-like Element of Funcs (P)
B * x is Relation-like Function-like set
o1 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o1) is functional non empty set
the carrier of o1 is non empty set
id the carrier of o1 is Relation-like the carrier of o1 -defined the carrier of o1 -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of o1) quasi_total onto bijective Element of bool [: the carrier of o1, the carrier of o1:]
[: the carrier of o1, the carrier of o1:] is non empty set
bool [: the carrier of o1, the carrier of o1:] is non empty set
A is Relation-like Function-like Element of Funcs (P)
x is Relation-like Function-like Element of Funcs (P)
B is non empty V65() reflexive transitive antisymmetric (P)
(B,o1) is functional set
x * A is Relation-like Function-like set
the carrier of B is non empty set
[: the carrier of B, the carrier of o1:] is non empty set
bool [: the carrier of B, the carrier of o1:] is non empty set
Funcs ( the carrier of B, the carrier of o1) is functional non empty FUNCTION_DOMAIN of the carrier of B, the carrier of o1
j is Relation-like the carrier of B -defined the carrier of o1 -valued Function-like non empty V24( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of o1:]
e is Relation-like the carrier of B -defined the carrier of o1 -valued Function-like non empty V24( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of o1:]
rng e is Element of bool the carrier of o1
bool the carrier of o1 is non empty set
(o1,B) is functional set
A * x is Relation-like Function-like set
the carrier of B is non empty set
[: the carrier of o1, the carrier of B:] is non empty set
bool [: the carrier of o1, the carrier of B:] is non empty set
Funcs ( the carrier of o1, the carrier of B) is functional non empty FUNCTION_DOMAIN of the carrier of o1, the carrier of B
j is Relation-like the carrier of o1 -defined the carrier of B -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of B:]
e is Relation-like the carrier of o1 -defined the carrier of B -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of B:]
dom e is Element of bool the carrier of o1
bool the carrier of o1 is non empty set
x is Relation-like Function-like Element of Funcs (P)
B is non empty V65() reflexive transitive antisymmetric (P)
(o1,B) is functional set
A * x is Relation-like Function-like set
j is Relation-like Function-like Element of Funcs (P)
e is non empty V65() reflexive transitive antisymmetric (P)
(e,o1) is functional set
j * A is Relation-like Function-like set
x is Relation-like Function-like Element of Funcs (P)
o1 is non empty V65() reflexive transitive antisymmetric (P)
o2 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o2) is functional set
e is Relation-like Function-like Element of Funcs (P)
A is non empty V65() reflexive transitive antisymmetric (P)
(o2,A) is functional set
j is Relation-like Function-like Element of Funcs (P)
B is non empty V65() reflexive transitive antisymmetric (P)
(A,B) is functional set
x * e is Relation-like Function-like set
(x * e) * j is Relation-like Function-like set
e * j is Relation-like Function-like set
x * (e * j) is Relation-like Function-like set
o1 is non empty non void V62() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms CatStr
the carrier of o1 is non empty set
the carrier' of o1 is non empty set
o1 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o1) is functional non empty set
the carrier of o1 is non empty set
id the carrier of o1 is Relation-like the carrier of o1 -defined the carrier of o1 -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of o1) quasi_total onto bijective Element of bool [: the carrier of o1, the carrier of o1:]
[: the carrier of o1, the carrier of o1:] is non empty set
bool [: the carrier of o1, the carrier of o1:] is non empty set
x is Relation-like Function-like Element of Funcs (P)
B is non empty V65() reflexive transitive antisymmetric (P)
(B,o1) is functional set
A is Relation-like Function-like Element of Funcs (P)
x * A is Relation-like Function-like set
the carrier of B is non empty set
[: the carrier of B, the carrier of o1:] is non empty set
bool [: the carrier of B, the carrier of o1:] is non empty set
Funcs ( the carrier of B, the carrier of o1) is functional non empty FUNCTION_DOMAIN of the carrier of B, the carrier of o1
j is Relation-like the carrier of B -defined the carrier of o1 -valued Function-like non empty V24( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of o1:]
e is Relation-like the carrier of B -defined the carrier of o1 -valued Function-like non empty V24( the carrier of B) quasi_total Element of bool [: the carrier of B, the carrier of o1:]
rng e is Element of bool the carrier of o1
bool the carrier of o1 is non empty set
(o1,B) is functional set
A * x is Relation-like Function-like set
the carrier of B is non empty set
[: the carrier of o1, the carrier of B:] is non empty set
bool [: the carrier of o1, the carrier of B:] is non empty set
Funcs ( the carrier of o1, the carrier of B) is functional non empty FUNCTION_DOMAIN of the carrier of o1, the carrier of B
j is Relation-like the carrier of o1 -defined the carrier of B -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of B:]
e is Relation-like the carrier of o1 -defined the carrier of B -valued Function-like non empty V24( the carrier of o1) quasi_total Element of bool [: the carrier of o1, the carrier of B:]
dom e is Element of bool the carrier of o1
bool the carrier of o1 is non empty set
F1() is non empty set
[:F1(),F1():] is non empty set
P is Relation-like [:F1(),F1():] -defined Function-like V24([:F1(),F1():]) set
[:F1(),F1(),F1():] is non empty set
o1 is Relation-like [:F1(),F1(),F1():] -defined Function-like V24([:F1(),F1(),F1():]) set
o2 is set
dom o1 is set
o1 . o2 is set
dom o1 is Element of bool [:F1(),F1(),F1():]
bool [:F1(),F1(),F1():] is non empty set
A is set
B is set
x is set
[A,B,x] is V25() V26() set
[A,B] is V25() set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
[[A,B],x] is V25() set
{[A,B],x} is non empty set
{[A,B]} is Function-like non empty set
{{[A,B],x},{[A,B]}} is non empty set
o1 . (A,B,x) is set
F2(A,B) is functional set
F2(B,x) is functional set
FuncComp (F2(A,B),F2(B,x)) is Relation-like [:F2(B,x),F2(A,B):] -defined Function-like V24([:F2(B,x),F2(A,B):]) Function-yielding compositional set
[:F2(B,x),F2(A,B):] is set
A is set
B is set
x is set
e is set
[B,x,e] is V25() V26() set
[B,x] is V25() set
{B,x} is non empty set
{B} is non empty set
{{B,x},{B}} is non empty set
[[B,x],e] is V25() set
{[B,x],e} is non empty set
{[B,x]} is Function-like non empty set
{{[B,x],e},{[B,x]}} is non empty set
P . (B,x) is set
F2(B,x) is functional set
F2(x,e) is functional set
[:F2(x,e),F2(B,x):] is set
P . (x,e) is set
[:(P . (x,e)),(P . (B,x)):] is set
{|P,P|} is Relation-like [:F1(),F1(),F1():] -defined Function-like V24([:F1(),F1(),F1():]) set
{|P,P|} . (B,x,e) is set
{|P,P|} . A is set
{|P|} is Relation-like [:F1(),F1(),F1():] -defined Function-like V24([:F1(),F1(),F1():]) set
{|P|} . A is set
{|P|} . (B,x,e) is set
P . (B,e) is set
j is set
f is set
j9 is set
[f,j9] is V25() set
{f,j9} is non empty set
{f} is non empty set
{{f,j9},{f}} is non empty set
f9 is Relation-like Function-like set
e9 is Relation-like Function-like set
f9 * e9 is Relation-like Function-like set
F2(B,e) is functional set
o2 is Relation-like [:F1(),F1(),F1():] -defined Function-like V24([:F1(),F1(),F1():]) Function-yielding set
o2 . A is set
o2 . (B,x,e) is set
FuncComp (F2(B,x),F2(x,e)) is Relation-like [:F2(x,e),F2(B,x):] -defined Function-like V24([:F2(x,e),F2(B,x):]) Function-yielding compositional set
j is Relation-like Function-like set
dom j is set
rng (FuncComp (F2(B,x),F2(x,e))) is set
j9 is set
dom (FuncComp (F2(B,x),F2(x,e))) is Relation-like F2(x,e) -defined F2(B,x) -valued Element of bool [:F2(x,e),F2(B,x):]
bool [:F2(x,e),F2(B,x):] is non empty set
f9 is set
(FuncComp (F2(B,x),F2(x,e))) . f9 is set
j9 is Relation-like Function-like set
e9 is Relation-like Function-like set
[j9,e9] is V25() set
{j9,e9} is functional non empty set
{j9} is functional non empty set
{{j9,e9},{j9}} is non empty set
e9 * j9 is Relation-like Function-like set
rng j is set
[:({|P,P|} . A),({|P|} . A):] is set
bool [:({|P,P|} . A),({|P|} . A):] is non empty set
A is Relation-like [:F1(),F1(),F1():] -defined Function-like V24([:F1(),F1(),F1():]) ManySortedFunction of {|P,P|},{|P|}
AltCatStr(# F1(),P,A #) is non empty strict AltCatStr
the carrier of AltCatStr(# F1(),P,A #) is non empty set
the Arrows of AltCatStr(# F1(),P,A #) is Relation-like [: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] -defined Function-like V24([: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):]) set
[: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] is non empty set
the Comp of AltCatStr(# F1(),P,A #) is Relation-like [: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] -defined Function-like V24([: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):]) ManySortedFunction of {| the Arrows of AltCatStr(# F1(),P,A #), the Arrows of AltCatStr(# F1(),P,A #)|},{| the Arrows of AltCatStr(# F1(),P,A #)|}
[: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] is non empty set
{| the Arrows of AltCatStr(# F1(),P,A #), the Arrows of AltCatStr(# F1(),P,A #)|} is Relation-like [: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] -defined Function-like V24([: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):]) set
{| the Arrows of AltCatStr(# F1(),P,A #)|} is Relation-like [: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):] -defined Function-like V24([: the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #), the carrier of AltCatStr(# F1(),P,A #):]) set
x is Element of F1()
e is Element of F1()
the Arrows of AltCatStr(# F1(),P,A #) . (x,e) is set
F2(x,e) is functional set
j is Element of F1()
f is Element of F1()
j9 is Element of F1()
the Comp of AltCatStr(# F1(),P,A #) . (j,f,j9) is set
F2(j,f) is functional set
F2(f,j9) is functional set
FuncComp (F2(j,f),F2(f,j9)) is Relation-like [:F2(f,j9),F2(j,f):] -defined Function-like V24([:F2(f,j9),F2(j,f):]) Function-yielding compositional set
[:F2(f,j9),F2(j,f):] is set
F1() is non empty set
P is strict AltCatStr
the carrier of P is set
the Arrows of P is Relation-like [: the carrier of P, the carrier of P:] -defined Function-like V24([: the carrier of P, the carrier of P:]) set
[: the carrier of P, the carrier of P:] is set
the Comp of P is Relation-like [: the carrier of P, the carrier of P, the carrier of P:] -defined Function-like V24([: the carrier of P, the carrier of P, the carrier of P:]) ManySortedFunction of {| the Arrows of P, the Arrows of P|},{| the Arrows of P|}
[: the carrier of P, the carrier of P, the carrier of P:] is set
{| the Arrows of P, the Arrows of P|} is Relation-like [: the carrier of P, the carrier of P, the carrier of P:] -defined Function-like V24([: the carrier of P, the carrier of P, the carrier of P:]) set
{| the Arrows of P|} is Relation-like [: the carrier of P, the carrier of P, the carrier of P:] -defined Function-like V24([: the carrier of P, the carrier of P, the carrier of P:]) set
o1 is strict AltCatStr
the carrier of o1 is set
the Arrows of o1 is Relation-like [: the carrier of o1, the carrier of o1:] -defined Function-like V24([: the carrier of o1, the carrier of o1:]) set
[: the carrier of o1, the carrier of o1:] is set
the Comp of o1 is Relation-like [: the carrier of o1, the carrier of o1, the carrier of o1:] -defined Function-like V24([: the carrier of o1, the carrier of o1, the carrier of o1:]) ManySortedFunction of {| the Arrows of o1, the Arrows of o1|},{| the Arrows of o1|}
[: the carrier of o1, the carrier of o1, the carrier of o1:] is set
{| the Arrows of o1, the Arrows of o1|} is Relation-like [: the carrier of o1, the carrier of o1, the carrier of o1:] -defined Function-like V24([: the carrier of o1, the carrier of o1, the carrier of o1:]) set
{| the Arrows of o1|} is Relation-like [: the carrier of o1, the carrier of o1, the carrier of o1:] -defined Function-like V24([: the carrier of o1, the carrier of o1, the carrier of o1:]) set
o2 is set
A is set
B is set
the Comp of P . (o2,A,B) is set
F2(o2,A) is functional set
F2(A,B) is functional set
FuncComp (F2(o2,A),F2(A,B)) is Relation-like [:F2(A,B),F2(o2,A):] -defined Function-like V24([:F2(A,B),F2(o2,A):]) Function-yielding compositional set
[:F2(A,B),F2(o2,A):] is set
the Comp of o1 . (o2,A,B) is set
o2 is Element of F1()
A is Element of F1()
the Arrows of P . (o2,A) is set
F2(o2,A) is functional set
the Arrows of o1 . (o2,A) is set
P is non empty () set
B is Relation-like Function-like set
o1 is non empty V65() reflexive transitive antisymmetric (P)
o2 is non empty V65() reflexive transitive antisymmetric (P)
(o1,o2) is functional set
x is Relation-like Function-like set
A is non empty V65() reflexive transitive antisymmetric (P)
(o2,A) is functional set
B * x is Relation-like Function-like set
(o1,A) is functional set
P is non empty () set
(P) is strict AltCatStr
the carrier of (P) is set
o2 is Element of the carrier of (P)
A is Element of the carrier of (P)
<^o2,A^> is set
the Arrows of (P) is Relation-like [: the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P):]) set
[: the carrier of (P), the carrier of (P):] is set
the Arrows of (P) . (o2,A) is set
B is Element of the carrier of (P)
<^A,B^> is set
the Arrows of (P) . (A,B) is set
<^o2,B^> is set
the Arrows of (P) . (o2,B) is set
x is non empty V65() reflexive transitive antisymmetric (P)
e is non empty V65() reflexive transitive antisymmetric (P)
(x,e) is functional set
f is set
j is non empty V65() reflexive transitive antisymmetric (P)
(e,j) is functional set
j9 is set
f9 is Relation-like Function-like set
e9 is Relation-like Function-like set
f9 * e9 is Relation-like Function-like set
(x,j) is functional set
P is non empty () set
(P) is non empty transitive strict AltCatStr
the Arrows of (P) is Relation-like [: the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P):]) set
the carrier of (P) is non empty set
[: the carrier of (P), the carrier of (P):] is non empty set
the Comp of (P) is Relation-like [: the carrier of (P), the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P), the carrier of (P):]) ManySortedFunction of {| the Arrows of (P), the Arrows of (P)|},{| the Arrows of (P)|}
[: the carrier of (P), the carrier of (P), the carrier of (P):] is non empty set
{| the Arrows of (P), the Arrows of (P)|} is Relation-like [: the carrier of (P), the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P), the carrier of (P):]) set
{| the Arrows of (P)|} is Relation-like [: the carrier of (P), the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P), the carrier of (P):]) set
B is Element of the carrier of (P)
x is Element of the carrier of (P)
the Arrows of (P) . (B,x) is set
e is Element of the carrier of (P)
the Arrows of (P) . (x,e) is set
j is Element of the carrier of (P)
the Arrows of (P) . (e,j) is set
the Comp of (P) . (B,e,j) is Relation-like [:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (B,e)):] -defined the Arrows of (P) . (B,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (B,e)):],( the Arrows of (P) . (B,j)):]
the Arrows of (P) . (B,e) is set
[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (B,e)):] is set
the Arrows of (P) . (B,j) is set
[:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (B,e)):],( the Arrows of (P) . (B,j)):] is set
bool [:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (B,e)):],( the Arrows of (P) . (B,j)):] is non empty set
the Comp of (P) . (B,x,e) is Relation-like [:( the Arrows of (P) . (x,e)),( the Arrows of (P) . (B,x)):] -defined the Arrows of (P) . (B,e) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (x,e)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,e)):]
[:( the Arrows of (P) . (x,e)),( the Arrows of (P) . (B,x)):] is set
[:[:( the Arrows of (P) . (x,e)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,e)):] is set
bool [:[:( the Arrows of (P) . (x,e)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,e)):] is non empty set
the Comp of (P) . (B,x,j) is Relation-like [:( the Arrows of (P) . (x,j)),( the Arrows of (P) . (B,x)):] -defined the Arrows of (P) . (B,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (x,j)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,j)):]
the Arrows of (P) . (x,j) is set
[:( the Arrows of (P) . (x,j)),( the Arrows of (P) . (B,x)):] is set
[:[:( the Arrows of (P) . (x,j)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,j)):] is set
bool [:[:( the Arrows of (P) . (x,j)),( the Arrows of (P) . (B,x)):],( the Arrows of (P) . (B,j)):] is non empty set
the Comp of (P) . (x,e,j) is Relation-like [:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (x,e)):] -defined the Arrows of (P) . (x,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (x,e)):],( the Arrows of (P) . (x,j)):]
[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (x,e)):] is set
[:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (x,e)):],( the Arrows of (P) . (x,j)):] is set
bool [:[:( the Arrows of (P) . (e,j)),( the Arrows of (P) . (x,e)):],( the Arrows of (P) . (x,j)):] is non empty set
f is set
j9 is set
f9 is set
( the Comp of (P) . (B,x,e)) . (j9,f) is set
( the Comp of (P) . (B,e,j)) . (f9,(( the Comp of (P) . (B,x,e)) . (j9,f))) is set
( the Comp of (P) . (x,e,j)) . (f9,j9) is set
( the Comp of (P) . (B,x,j)) . ((( the Comp of (P) . (x,e,j)) . (f9,j9)),f) is set
j9 is non empty V65() reflexive transitive antisymmetric (P)
k9 is non empty V65() reflexive transitive antisymmetric (P)
(j9,k9) is functional set
l9 is non empty V65() reflexive transitive antisymmetric (P)
(k9,l9) is functional set
e9 is non empty V65() reflexive transitive antisymmetric (P)
(e9,j9) is functional set
(j9,l9) is functional set
FuncComp ((e9,j9),(j9,l9)) is Relation-like [:(j9,l9),(e9,j9):] -defined Function-like V24([:(j9,l9),(e9,j9):]) Function-yielding compositional set
[:(j9,l9),(e9,j9):] is set
FuncComp ((j9,k9),(k9,l9)) is Relation-like [:(k9,l9),(j9,k9):] -defined Function-like V24([:(k9,l9),(j9,k9):]) Function-yielding compositional set
[:(k9,l9),(j9,k9):] is set
g9 is Relation-like Function-like set
h9 is Relation-like Function-like set
g9 * h9 is Relation-like Function-like set
FuncComp ((e9,j9),(j9,k9)) is Relation-like [:(j9,k9),(e9,j9):] -defined Function-like V24([:(j9,k9),(e9,j9):]) Function-yielding compositional set
[:(j9,k9),(e9,j9):] is set
f9 is Relation-like Function-like set
f9 * g9 is Relation-like Function-like set
( the Comp of (P) . (B,x,j)) . ((g9 * h9),f9) is set
f9 * (g9 * h9) is Relation-like Function-like set
(e9,k9) is functional set
FuncComp ((e9,k9),(k9,l9)) is Relation-like [:(k9,l9),(e9,k9):] -defined Function-like V24([:(k9,l9),(e9,k9):]) Function-yielding compositional set
[:(k9,l9),(e9,k9):] is set
( the Comp of (P) . (B,e,j)) . (f9,(f9 * g9)) is set
(f9 * g9) * h9 is Relation-like Function-like set
B is Element of the carrier of (P)
the Arrows of (P) . (B,B) is set
x is non empty V65() reflexive transitive antisymmetric (P)
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
id the carrier of x is Relation-like the carrier of x -defined the carrier of x -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of x) quasi_total onto bijective Element of bool [: the carrier of x, the carrier of x:]
e is Relation-like the carrier of x -defined the carrier of x -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of x) quasi_total onto bijective Element of bool [: the carrier of x, the carrier of x:]
(x,x) is functional non empty set
j is Element of the carrier of (P)
the Arrows of (P) . (j,B) is set
the Comp of (P) . (j,B,B) is Relation-like [:( the Arrows of (P) . (B,B)),( the Arrows of (P) . (j,B)):] -defined the Arrows of (P) . (j,B) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (B,B)),( the Arrows of (P) . (j,B)):],( the Arrows of (P) . (j,B)):]
[:( the Arrows of (P) . (B,B)),( the Arrows of (P) . (j,B)):] is set
[:[:( the Arrows of (P) . (B,B)),( the Arrows of (P) . (j,B)):],( the Arrows of (P) . (j,B)):] is set
bool [:[:( the Arrows of (P) . (B,B)),( the Arrows of (P) . (j,B)):],( the Arrows of (P) . (j,B)):] is non empty set
f is set
( the Comp of (P) . (j,B,B)) . (e,f) is set
j9 is non empty V65() reflexive transitive antisymmetric (P)
(j9,x) is functional set
FuncComp ((j9,x),(x,x)) is Relation-like [:(x,x),(j9,x):] -defined Function-like V24([:(x,x),(j9,x):]) Function-yielding compositional set
[:(x,x),(j9,x):] is set
the carrier of j9 is non empty set
[: the carrier of j9, the carrier of x:] is non empty set
bool [: the carrier of j9, the carrier of x:] is non empty set
Funcs ( the carrier of j9, the carrier of x) is functional non empty FUNCTION_DOMAIN of the carrier of j9, the carrier of x
f9 is Relation-like the carrier of j9 -defined the carrier of x -valued Function-like non empty V24( the carrier of j9) quasi_total Element of bool [: the carrier of j9, the carrier of x:]
Funcs ( the carrier of x, the carrier of x) is functional non empty FUNCTION_DOMAIN of the carrier of x, the carrier of x
e9 is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V24( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
rng f9 is Element of bool the carrier of x
bool the carrier of x is non empty set
e9 * f9 is Relation-like the carrier of j9 -defined the carrier of x -valued Function-like non empty V24( the carrier of j9) quasi_total Element of bool [: the carrier of j9, the carrier of x:]
B is Element of the carrier of (P)
the Arrows of (P) . (B,B) is set
x is non empty V65() reflexive transitive antisymmetric (P)
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
id the carrier of x is Relation-like the carrier of x -defined the carrier of x -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of x) quasi_total onto bijective Element of bool [: the carrier of x, the carrier of x:]
e is Relation-like the carrier of x -defined the carrier of x -valued V6() V8() V9() V13() Function-like one-to-one non empty V24( the carrier of x) quasi_total onto bijective Element of bool [: the carrier of x, the carrier of x:]
(x,x) is functional non empty set
j is Element of the carrier of (P)
the Arrows of (P) . (B,j) is set
the Comp of (P) . (B,B,j) is Relation-like [:( the Arrows of (P) . (B,j)),( the Arrows of (P) . (B,B)):] -defined the Arrows of (P) . (B,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (P) . (B,j)),( the Arrows of (P) . (B,B)):],( the Arrows of (P) . (B,j)):]
[:( the Arrows of (P) . (B,j)),( the Arrows of (P) . (B,B)):] is set
[:[:( the Arrows of (P) . (B,j)),( the Arrows of (P) . (B,B)):],( the Arrows of (P) . (B,j)):] is set
bool [:[:( the Arrows of (P) . (B,j)),( the Arrows of (P) . (B,B)):],( the Arrows of (P) . (B,j)):] is non empty set
f is set
( the Comp of (P) . (B,B,j)) . (f,e) is set
j9 is non empty V65() reflexive transitive antisymmetric (P)
(x,j9) is functional set
FuncComp ((x,x),(x,j9)) is Relation-like [:(x,j9),(x,x):] -defined Function-like V24([:(x,j9),(x,x):]) Function-yielding compositional set
[:(x,j9),(x,x):] is set
the carrier of j9 is non empty set
[: the carrier of x, the carrier of j9:] is non empty set
bool [: the carrier of x, the carrier of j9:] is non empty set
Funcs ( the carrier of x, the carrier of j9) is functional non empty FUNCTION_DOMAIN of the carrier of x, the carrier of j9
f9 is Relation-like the carrier of x -defined the carrier of j9 -valued Function-like non empty V24( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of j9:]
Funcs ( the carrier of x, the carrier of x) is functional non empty FUNCTION_DOMAIN of the carrier of x, the carrier of x
e9 is Relation-like the carrier of x -defined the carrier of x -valued Function-like non empty V24( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of x:]
dom f9 is Element of bool the carrier of x
bool the carrier of x is non empty set
f9 * e9 is Relation-like the carrier of x -defined the carrier of j9 -valued Function-like non empty V24( the carrier of x) quasi_total Element of bool [: the carrier of x, the carrier of j9:]
P is non empty () set
(P) is non empty transitive strict associative with_units AltCatStr
the carrier of (P) is non empty set
o1 is Element of the carrier of (P)
o2 is Element of the carrier of (P)
<^o1,o2^> is set
the Arrows of (P) is Relation-like [: the carrier of (P), the carrier of (P):] -defined Function-like V24([: the carrier of (P), the carrier of (P):]) set
[: the carrier of (P), the carrier of (P):] is non empty set
the Arrows of (P) . (o1,o2) is set
A is non empty V65() reflexive transitive antisymmetric (P)
B is non empty V65() reflexive transitive antisymmetric (P)
the carrier of A is non empty set
the carrier of B is non empty set
Funcs ( the carrier of A, the carrier of B) is functional non empty FUNCTION_DOMAIN of the carrier of A, the carrier of B
x is set
(A,B) is functional set
[: the carrier of A, the carrier of B:] is non empty set
bool [: the carrier of A, the carrier of B:] is non empty set
e is Relation-like the carrier of A -defined the carrier of B -valued Function-like non empty V24( the carrier of A) quasi_total Element of bool [: the carrier of A, the carrier of B:]