:: ORDERS_3 semantic presentation

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

F

[:F

P is Relation-like [:F

[:F

o1 is Relation-like [:F

o2 is set

dom o1 is set

o1 . o2 is set

dom o1 is Element of bool [:F

bool [:F

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

F

F

FuncComp (F

[:F

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

F

F

[:F

P . (x,e) is set

[:(P . (x,e)),(P . (B,x)):] is set

{|P,P|} is Relation-like [:F

{|P,P|} . (B,x,e) is set

{|P,P|} . A is set

{|P|} is Relation-like [:F

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

F

o2 is Relation-like [:F

o2 . A is set

o2 . (B,x,e) is set

FuncComp (F

j is Relation-like Function-like set

dom j is set

rng (FuncComp (F

j9 is set

dom (FuncComp (F

bool [:F

f9 is set

(FuncComp (F

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

AltCatStr(# F

the carrier of AltCatStr(# F

the Arrows of AltCatStr(# F

[: the carrier of AltCatStr(# F

the Comp of AltCatStr(# F

[: the carrier of AltCatStr(# F

{| the Arrows of AltCatStr(# F

{| the Arrows of AltCatStr(# F

x is Element of F

e is Element of F

the Arrows of AltCatStr(# F

F

j is Element of F

f is Element of F

j9 is Element of F

the Comp of AltCatStr(# F

F

F

FuncComp (F

[:F

F

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

F

F

FuncComp (F

[:F

the Comp of o1 . (o2,A,B) is set

o2 is Element of F

A is Element of F

the Arrows of P . (o2,A) is set

F

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