:: CAT_4 semantic presentation

K93() is set

K97() is non empty non trivial V24() V25() V26() non finite cardinal limit_cardinal Element of bool K93()

bool K93() is set

K92() is non empty non trivial V24() V25() V26() non finite cardinal limit_cardinal set

bool K92() is non trivial non finite set

bool K97() is non trivial non finite set

{} is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() finite V40() cardinal {} -element set

1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K97()

card {} is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() finite V40() cardinal {} -element set

C is non empty non void V57() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

a is Element of the carrier of C

c is Element of the carrier of C

Hom (a,c) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

Hom (c,a) is Element of bool the carrier' of C

{ b

id c is Morphism of c,c

id a is Morphism of a,a

d is Morphism of c,a

b is Morphism of a,c

b * d is Morphism of c,c

d * b is Morphism of a,a

C is non empty non void V57() Category-like transitive associative reflexive with_identities CatStr

the carrier of C is non empty set

the carrier' of C is non empty set

[:{}, the carrier of C:] is set

bool [:{}, the carrier of C:] is set

a is Relation-like {} -defined the carrier of C -valued Function-like one-to-one constant functional empty total V18( {} , the carrier of C) V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() finite finite-yielding V40() cardinal {} -element Element of bool [:{}, the carrier of C:]

c is Element of the carrier of C

b is Relation-like {} -defined the carrier' of C -valued Function-like one-to-one constant functional empty total V18( {} , the carrier' of C) V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() finite finite-yielding V40() cardinal {} -element Projections_family of c, {}

cods b is Relation-like {} -defined the carrier of C -valued Function-like one-to-one constant functional empty total V18( {} , the carrier of C) V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() finite finite-yielding V40() cardinal {} -element Element of bool [:{}, the carrier of C:]

d is Element of the carrier of C

e is Element of the carrier of C

({},1) --> (d,e) is Relation-like {{},1} -defined the carrier of C -valued Function-like non empty total V18({{},1}, the carrier of C) finite Element of bool [:{{},1}, the carrier of C:]

{{},1} is non empty finite V40() set

[:{{},1}, the carrier of C:] is set

bool [:{{},1}, the carrier of C:] is set

f is Element of the carrier of C

h is Relation-like {{},1} -defined the carrier' of C -valued Function-like non empty total V18({{},1}, the carrier' of C) finite Projections_family of f,{{},1}

cods h is Relation-like {{},1} -defined the carrier of C -valued Function-like non empty total V18({{},1}, the carrier of C) finite Element of bool [:{{},1}, the carrier of C:]

h /. {} is Element of the carrier' of C

g is Element of the carrier' of C

dom g is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

bool [: the carrier' of C, the carrier of C:] is set

the Source of C . g is Element of the carrier of C

cod g is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . g is Element of the carrier of C

h /. 1 is Element of the carrier' of C

k is Element of the carrier' of C

dom k is Element of the carrier of C

the Source of C . k is Element of the carrier of C

cod k is Element of the carrier of C

the Target of C . k is Element of the carrier of C

h . 1 is set

(({},1) --> (d,e)) /. {} is Element of the carrier of C

(({},1) --> (d,e)) /. 1 is Element of the carrier of C

dom h is finite V40() Element of bool {{},1}

bool {{},1} is finite V40() set

h . {} is set

({},1) --> (g,k) is Relation-like {{},1} -defined the carrier' of C -valued Function-like non empty total V18({{},1}, the carrier' of C) finite Element of bool [:{{},1}, the carrier' of C:]

[:{{},1}, the carrier' of C:] is set

bool [:{{},1}, the carrier' of C:] is set

a is Element of the carrier of C

c is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal set

c + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal set

b is finite set

[:b, the carrier of C:] is set

bool [:b, the carrier of C:] is set

card b is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K92()

d is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

the Element of b is Element of b

{ the Element of b} is non empty trivial finite 1 -element set

b \ { the Element of b} is finite Element of bool b

bool b is finite V40() set

[:(b \ { the Element of b}), the carrier of C:] is set

bool [:(b \ { the Element of b}), the carrier of C:] is set

d | (b \ { the Element of b}) is Relation-like b -defined the carrier of C -valued Function-like finite Element of bool [:b, the carrier of C:]

s is finite set

card s is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K92()

f is finite set

card f is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K92()

(card b) - (card f) is V31() V32() V33() set

(card b) - 1 is V31() V32() V33() set

h is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

g is Element of the carrier of C

k is Relation-like b \ { the Element of b} -defined the carrier' of C -valued Function-like total V18(b \ { the Element of b}, the carrier' of C) finite Projections_family of g,b \ { the Element of b}

cods k is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

d /. the Element of b is Element of the carrier of C

c is Element of the carrier' of C

dom c is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is set

bool [: the carrier' of C, the carrier of C:] is set

the Source of C . c is Element of the carrier of C

b is Element of the carrier of C

i1 is Element of the carrier' of C

dom i1 is Element of the carrier of C

the Source of C . i1 is Element of the carrier of C

cod c is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V18( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . c is Element of the carrier of C

cod i1 is Element of the carrier of C

the Target of C . i1 is Element of the carrier of C

k * c is Relation-like b \ { the Element of b} -defined the carrier' of C -valued Function-like total V18(b \ { the Element of b}, the carrier' of C) finite Element of bool [:(b \ { the Element of b}), the carrier' of C:]

[:(b \ { the Element of b}), the carrier' of C:] is set

bool [:(b \ { the Element of b}), the carrier' of C:] is set

the Element of b .--> i1 is Relation-like { the Element of b} -defined the carrier' of C -valued Function-like non empty total V18({ the Element of b}, the carrier' of C) finite Element of bool [:{ the Element of b}, the carrier' of C:]

[:{ the Element of b}, the carrier' of C:] is set

bool [:{ the Element of b}, the carrier' of C:] is set

{ the Element of b} --> i1 is Relation-like { the Element of b} -defined {i1} -valued Function-like non empty total V18({ the Element of b},{i1}) finite Element of bool [:{ the Element of b},{i1}:]

{i1} is non empty trivial finite 1 -element set

[:{ the Element of b},{i1}:] is finite set

bool [:{ the Element of b},{i1}:] is finite V40() set

(k * c) +* ( the Element of b .--> i1) is Relation-like Function-like finite set

{ the Element of b} --> i1 is Relation-like { the Element of b} -defined the carrier' of C -valued Function-like non empty total V18({ the Element of b}, the carrier' of C) finite Element of bool [:{ the Element of b}, the carrier' of C:]

dom ({ the Element of b} --> i1) is finite Element of bool { the Element of b}

bool { the Element of b} is finite V40() set

rng ((k * c) +* ( the Element of b .--> i1)) is finite set

rng (k * c) is finite Element of bool the carrier' of C

bool the carrier' of C is set

rng ( the Element of b .--> i1) is finite Element of bool the carrier' of C

(rng (k * c)) \/ (rng ( the Element of b .--> i1)) is finite Element of bool the carrier' of C

dom (k * c) is finite Element of bool (b \ { the Element of b})

bool (b \ { the Element of b}) is finite V40() set

dom ( the Element of b .--> i1) is finite Element of bool { the Element of b}

(dom (k * c)) \/ (dom ( the Element of b .--> i1)) is finite set

b \/ { the Element of b} is non empty finite set

dom ((k * c) +* ( the Element of b .--> i1)) is finite set

[:b, the carrier' of C:] is set

bool [:b, the carrier' of C:] is set

doms k is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

(b \ { the Element of b}) --> g is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

{g} is non empty trivial finite 1 -element set

[:(b \ { the Element of b}),{g}:] is finite set

F9 is set

F9 is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Element of bool [:b, the carrier' of C:]

F9 /. F9 is Element of the carrier' of C

F9 . F9 is set

( the Element of b .--> i1) . F9 is set

b --> b is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

{b} is non empty trivial finite 1 -element set

[:b,{b}:] is finite set

(b --> b) . F9 is set

dom (F9 /. F9) is Element of the carrier of C

the Source of C . (F9 /. F9) is Element of the carrier of C

doms F9 is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

(doms F9) /. F9 is Element of the carrier of C

F9 is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Element of bool [:b, the carrier' of C:]

F9 /. F9 is Element of the carrier' of C

F9 . F9 is set

(k * c) . F9 is set

(k * c) /. F9 is Element of the carrier' of C

doms F9 is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

(doms F9) /. F9 is Element of the carrier of C

dom ((k * c) /. F9) is Element of the carrier of C

the Source of C . ((k * c) /. F9) is Element of the carrier of C

doms (k * c) is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

(doms (k * c)) /. F9 is Element of the carrier of C

(b \ { the Element of b}) --> b is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

{b} is non empty trivial finite 1 -element set

[:(b \ { the Element of b}),{b}:] is finite set

((b \ { the Element of b}) --> b) /. F9 is Element of the carrier of C

b --> b is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

[:b,{b}:] is finite set

(b --> b) . F9 is set

b --> b is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

{b} is non empty trivial finite 1 -element set

[:b,{b}:] is finite set

(b --> b) . F9 is set

F9 is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Element of bool [:b, the carrier' of C:]

doms F9 is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

(doms F9) /. F9 is Element of the carrier of C

b --> b is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

{b} is non empty trivial finite 1 -element set

[:b,{b}:] is finite set

(b --> b) . F9 is set

F9 is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Element of bool [:b, the carrier' of C:]

doms F9 is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

(doms F9) /. F9 is Element of the carrier of C

(doms F9) . F9 is set

F9 is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Projections_family of b,b

cods F9 is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

F9 is set

F9 /. F9 is Element of the carrier' of C

F9 . F9 is set

( the Element of b .--> i1) . F9 is set

(cods F9) /. F9 is Element of the carrier of C

d /. F9 is Element of the carrier of C

F9 /. F9 is Element of the carrier' of C

F9 . F9 is set

(k * c) . F9 is set

(k * c) /. F9 is Element of the carrier' of C

(cods F9) /. F9 is Element of the carrier of C

cod ((k * c) /. F9) is Element of the carrier of C

the Target of C . ((k * c) /. F9) is Element of the carrier of C

cods (k * c) is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

(cods (k * c)) /. F9 is Element of the carrier of C

h /. F9 is Element of the carrier of C

h . F9 is set

d . F9 is set

d /. F9 is Element of the carrier of C

(cods F9) /. F9 is Element of the carrier of C

d /. F9 is Element of the carrier of C

(cods F9) /. F9 is Element of the carrier of C

d /. F9 is Element of the carrier of C

F9 is Element of the carrier of C

Hom (F9,b) is Element of bool the carrier' of C

{ b

d is Relation-like b -defined the carrier' of C -valued Function-like total V18(b, the carrier' of C) finite Projections_family of F9,b

cods d is Relation-like b -defined the carrier of C -valued Function-like total V18(b, the carrier of C) finite Element of bool [:b, the carrier of C:]

d | (b \ { the Element of b}) is Relation-like b -defined the carrier' of C -valued Function-like finite Element of bool [:b, the carrier' of C:]

G99 is set

F99 is Relation-like b \ { the Element of b} -defined the carrier' of C -valued Function-like total V18(b \ { the Element of b}, the carrier' of C) finite Element of bool [:(b \ { the Element of b}), the carrier' of C:]

F99 /. G99 is Element of the carrier' of C

F99 . G99 is set

d . G99 is set

d /. G99 is Element of the carrier' of C

doms F99 is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

(doms F99) /. G99 is Element of the carrier of C

dom (d /. G99) is Element of the carrier of C

the Source of C . (d /. G99) is Element of the carrier of C

(b \ { the Element of b}) --> F9 is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

{F9} is non empty trivial finite 1 -element set

[:(b \ { the Element of b}),{F9}:] is finite set

((b \ { the Element of b}) --> F9) /. G99 is Element of the carrier of C

G99 is set

h /. G99 is Element of the carrier of C

h . G99 is set

d . G99 is set

d /. G99 is Element of the carrier of C

d /. G99 is Element of the carrier' of C

d . G99 is set

G99 is Relation-like b \ { the Element of b} -defined the carrier' of C -valued Function-like total V18(b \ { the Element of b}, the carrier' of C) finite Projections_family of F9,b \ { the Element of b}

G99 . G99 is set

G99 /. G99 is Element of the carrier' of C

(cods k) /. G99 is Element of the carrier of C

cod (G99 /. G99) is Element of the carrier of C

the Target of C . (G99 /. G99) is Element of the carrier of C

cods G99 is Relation-like b \ { the Element of b} -defined the carrier of C -valued Function-like total V18(b \ { the Element of b}, the carrier of C) finite Element of bool [:(b \ { the Element of b}), the carrier of C:]

(cods G99) /. G99 is Element of the carrier of C

Hom (F9,g) is Element of bool the carrier' of C

{ b

G99 is Element of the carrier' of C

d /. the Element of b is Element of the carrier' of C

dom (d /. the Element of b) is Element of the carrier of C

the Source of C . (d /. the Element of b) is Element of the carrier of C

F9 /. the Element of b is Element of the carrier' of C

F9 . the Element of b is set

( the Element of b .--> i1) . the Element of b is set

(cods F9) /. the Element of b is Element of the carrier of C

cod (d /. the Element of b) is Element of the carrier of C

the Target of C . (d /. the Element of b) is Element of the carrier of C

Hom (F9,(cod i1)) is Element of bool the carrier' of C

{ b

g is Element of the carrier' of C

h is Element of the carrier' of C

cod h is Element of the carrier of C

the Target of C . h is Element of the carrier of C

c (*) h is Element of the carrier' of C

cod (c (*) h) is Element of the carrier of C

the Target of C . (c (*) h) is Element of the carrier of C

k is set

k /. k is Element of the carrier' of C

(k /. k) (*) (c (*) h) is Element of the carrier' of C

G99 /. k is Element of the carrier' of C

F9 /. k is Element of the carrier' of C

F9 . k is set

(k * c) . k is set

(k * c) /. k is Element of the carrier' of C

dom (k /. k) is Element of the carrier of C

the Source of C . (k /. k) is Element of the carrier of C

(k /. k) (*) c is Element of the carrier' of C

((k /. k) (*) c) (*) h is Element of the carrier' of C

((k * c) /. k) (*) h is Element of the carrier' of C

d /. k is Element of the carrier' of C

d . k is set

G99 . k is set

dom h is Element of the carrier of C

the Source of C . h is Element of the carrier of C

dom (c (*) h) is Element of the carrier of C

the Source of C . (c (*) h) is Element of the carrier of C

i1 (*) h is Element of the carrier' of C

k is set

F9 /. k is Element of the carrier' of C

(F9 /. k) (*) h is Element of the carrier' of C

d /. k is Element of the carrier' of C

F9 . k is set

( the Element of b .--> i1) . k is set

cod h is Element of the carrier of C

the Target of C . h is Element of the carrier of C

k /. k is Element of the carrier' of C

dom (k /. k) is Element of the carrier of C

the Source of C . (k /. k) is Element of the carrier of C

F9 . k is set

(k * c) . k is set

(k * c) /. k is Element of the carrier' of C

(k /. k) (*) c is Element of the carrier' of C

c (*) h is Element of the carrier' of C

(k /. k) (*) (c (*) h) is Element of the carrier' of C

(k /. k) (*) G99 is Element of the carrier' of C

G99 /. k is Element of the carrier' of C

G99 . k is set

d . k is set

c is finite set

[:c, the carrier of C:] is set

bool [:c, the carrier of C:] is set

b is Relation-like c -defined the carrier of C -valued Function-like total V18(c, the carrier of C) finite Element of bool [:c, the carrier of C:]

card c is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K92()

d is finite set

[:d, the carrier of C:] is set

bool [:d, the carrier of C:] is set

card d is V24() V25() V26() V30() V31() V32() V33() V35() finite cardinal Element of K92()

e is Relation-like d -defined the carrier of C -valued Function-like total V18(d, the carrier of C) finite Element of bool [:d, the carrier of C:]

[:{}, the carrier' of C:] is set

bool [:{}, the carrier' of C:] is set

s is Relation-like d -defined the carrier' of C -valued Function-like total V18(d, the carrier' of C) finite Projections_family of a,d

cods s is Relation-like d -defined the carrier of C -valued Function-like total V18(d, the carrier of C) finite Element of bool [:d, the carrier of C:]

f is set

(cods s) /. f is Element of the carrier of C

e /. f is Element of the carrier of C

the set is set

{ the set } is non empty trivial finite 1 -element set

the set :-> the set is Relation-like { the set } -defined { the set } -valued Function-like non empty total V18({ the set },{ the set }) finite Element of bool [:{ the set },{ the set }:]

[:{ the set },{ the set }:] is finite set

bool [:{ the set },{ the set }:] is finite V40() set

{ the set } --> the set is Relation-like { the set } -defined { the set } -valued Function-like non empty total V18({ the set },{ the set }) finite Element of bool [:{ the set },{ the set }:]

( the set , the set ) :-> the set is Relation-like [:{ the set },{ the set }:] -defined { the set } -valued Function-like total V18([:{ the set },{ the set }:],{ the set }) finite Element of bool [:[:{ the set },{ the set }:],{ the set }:]

[:[:{ the set },{ the set }:],{ the set }:] is finite set

bool [:[:{ the set },{ the set }:],{ the set }:] is finite V40() set

[ the set , the set ] is set

{[ the set , the set ]} is Function-like non empty trivial finite 1 -element set

{[ the set , the set ]} --> the set is Relation-like {[ the set , the set ]} -defined { the set } -valued Function-like non empty total V18({[ the set , the set ]},{ the set }) finite Element of bool [:{[ the set , the set ]},{ the set }:]

[:{[ the set , the set ]},{ the set }:] is finite set

bool [:{[ the set , the set ]},{ the set }:] is finite V40() set

Extract the set is Element of { the set }

({ the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set )) is () ()

C is non empty non void V57() ()

the of C is Element of the carrier of C

the carrier of C is non empty set

the of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like total V18([: the carrier of C, the carrier of C:], the carrier of C) Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]

[: the carrier of C, the carrier of C:] is set

[:[: the carrier of C, the carrier of C:], the carrier of C:] is set

bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set

a is Element of the carrier of C

c is Element of the carrier of C

the of C . (a,c) is Element of the carrier of C

the carrier' of C is non empty set

the of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier' of C -valued Function-like total V18([: the carrier of C, the carrier of C:], the carrier' of C) Element of bool [:[: the carrier of C, the carrier of C:], the carrier' of C:]

[:[: the carrier of C, the carrier of C:], the carrier' of C:] is set

bool [:[: the carrier of C, the carrier of C:], the carrier' of C:] is set

the of C . (a,c) is Element of the carrier' of C

the of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier' of C -valued Function-like total V18([: the carrier of C, the carrier of C:], the carrier' of C) Element of bool [:[: the carrier of C, the carrier of C:], the carrier' of C:]

the of C . (a,c) is Element of the carrier' of C

C is set

{C} is non empty trivial finite 1 -element set

a is set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

C is set

a is set

(C,a) is () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

C is set

a is set

(C,a) is non empty trivial finite non void 1 -element V57() trivial' transitive associative reflexive with_identities () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

the carrier of (C,a) is non empty trivial finite 1 -element set

the carrier' of (C,a) is non empty trivial finite 1 -element set

the Source of (C,a) is Relation-like the carrier' of (C,a) -defined the carrier of (C,a) -valued Function-like non empty total V18( the carrier' of (C,a), the carrier of (C,a)) finite Element of bool [: the carrier' of (C,a), the carrier of (C,a):]

[: the carrier' of (C,a), the carrier of (C,a):] is finite set

bool [: the carrier' of (C,a), the carrier of (C,a):] is finite V40() set

the Target of (C,a) is Relation-like the carrier' of (C,a) -defined the carrier of (C,a) -valued Function-like non empty total V18( the carrier' of (C,a), the carrier of (C,a)) finite Element of bool [: the carrier' of (C,a), the carrier of (C,a):]

the Comp of (C,a) is Relation-like [: the carrier' of (C,a), the carrier' of (C,a):] -defined the carrier' of (C,a) -valued Function-like finite Element of bool [:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):]

[: the carrier' of (C,a), the carrier' of (C,a):] is finite set

[:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):] is finite set

bool [:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):] is finite V40() set

CatStr(# the carrier of (C,a), the carrier' of (C,a), the Source of (C,a), the Target of (C,a), the Comp of (C,a) #) is strict CatStr

1Cat (C,a) is non empty trivial finite non void 1 -element V57() trivial' strict Category-like transitive associative reflexive with_identities CatStr

CatStr(# {C},{a},(a :-> C),(a :-> C),((a,a) :-> a) #) is strict CatStr

C is set

a is set

(C,a) is non empty trivial finite non void 1 -element V57() trivial' transitive associative reflexive with_identities () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

the Comp of (C,a) is Relation-like [: the carrier' of (C,a), the carrier' of (C,a):] -defined the carrier' of (C,a) -valued Function-like finite Element of bool [:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):]

the carrier' of (C,a) is non empty trivial finite 1 -element set

[: the carrier' of (C,a), the carrier' of (C,a):] is finite set

[:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):] is finite set

bool [:[: the carrier' of (C,a), the carrier' of (C,a):], the carrier' of (C,a):] is finite V40() set

the Source of (C,a) is Relation-like the carrier' of (C,a) -defined the carrier of (C,a) -valued Function-like non empty total V18( the carrier' of (C,a), the carrier of (C,a)) finite Element of bool [: the carrier' of (C,a), the carrier of (C,a):]

the carrier of (C,a) is non empty trivial finite 1 -element set

[: the carrier' of (C,a), the carrier of (C,a):] is finite set

bool [: the carrier' of (C,a), the carrier of (C,a):] is finite V40() set

the Target of (C,a) is Relation-like the carrier' of (C,a) -defined the carrier of (C,a) -valued Function-like non empty total V18( the carrier' of (C,a), the carrier of (C,a)) finite Element of bool [: the carrier' of (C,a), the carrier of (C,a):]

dom the Comp of (C,a) is Relation-like the carrier' of (C,a) -defined the carrier' of (C,a) -valued finite Element of bool [: the carrier' of (C,a), the carrier' of (C,a):]

bool [: the carrier' of (C,a), the carrier' of (C,a):] is finite V40() set

f is Element of the carrier' of (C,a)

s is Element of the carrier' of (C,a)

[f,s] is set

dom f is Element of the carrier of (C,a)

the Source of (C,a) . f is Element of the carrier of (C,a)

cod s is Element of the carrier of (C,a)

the Target of (C,a) . s is Element of the carrier of (C,a)

({},1) is non empty trivial finite non void 1 -element V57() trivial' transitive associative reflexive with_identities () ()

{{}} is non empty trivial finite V40() 1 -element set

{1} is non empty trivial finite V40() 1 -element set

1 :-> {} is Relation-like {1} -defined {{}} -valued Function-like non empty total V18({1},{{}}) finite Element of bool [:{1},{{}}:]

[:{1},{{}}:] is finite set

bool [:{1},{{}}:] is finite V40() set

{1} --> {} is Relation-like {1} -defined {{}} -valued Function-like non empty total V18({1},{{}}) finite Element of bool [:{1},{{}}:]

(1,1) :-> 1 is Relation-like [:{1},{1}:] -defined {1} -valued Function-like total V18([:{1},{1}:],{1}) finite Element of bool [:[:{1},{1}:],{1}:]

[:{1},{1}:] is finite set

[:[:{1},{1}:],{1}:] is finite set

bool [:[:{1},{1}:],{1}:] is finite V40() set

[1,1] is set

{[1,1]} is Function-like non empty trivial finite 1 -element set

{[1,1]} --> 1 is Relation-like {[1,1]} -defined {1} -valued Function-like non empty total V18({[1,1]},{1}) finite Element of bool [:{[1,1]},{1}:]

[:{[1,1]},{1}:] is finite set

bool [:{[1,1]},{1}:] is finite V40() set

Extract {} is finite Element of {{}}

({},{}) :-> {} is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like total V18([:{{}},{{}}:],{{}}) finite Element of bool [:[:{{}},{{}}:],{{}}:]

[:{{}},{{}}:] is finite set

[:[:{{}},{{}}:],{{}}:] is finite set

bool [:[:{{}},{{}}:],{{}}:] is finite V40() set

[{},{}] is set

{[{},{}]} is Function-like non empty trivial finite 1 -element set

{[{},{}]} --> {} is Relation-like {[{},{}]} -defined {{}} -valued Function-like non empty total V18({[{},{}]},{{}}) finite Element of bool [:{[{},{}]},{{}}:]

[:{[{},{}]},{{}}:] is finite set

bool [:{[{},{}]},{{}}:] is finite V40() set

({},{}) :-> 1 is Relation-like [:{{}},{{}}:] -defined {1} -valued Function-like total V18([:{{}},{{}}:],{1}) finite Element of bool [:[:{{}},{{}}:],{1}:]

[:[:{{}},{{}}:],{1}:] is finite set

bool [:[:{{}},{{}}:],{1}:] is finite V40() set

{[{},{}]} --> 1 is Relation-like {[{},{}]} -defined {1} -valued Function-like non empty total V18({[{},{}]},{1}) finite Element of bool [:{[{},{}]},{1}:]

[:{[{},{}]},{1}:] is finite set

bool [:{[{},{}]},{1}:] is finite V40() set

({{}},{1},(1 :-> {}),(1 :-> {}),((1,1) :-> 1),(Extract {}),(({},{}) :-> {}),(({},{}) :-> 1),(({},{}) :-> 1)) is () ()

C is set

a is set

(C,a) is non empty trivial finite non void 1 -element V57() trivial' transitive associative reflexive with_identities () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

C is set

a is set

(C,a) is non empty trivial finite non void 1 -element V57() trivial' Category-like transitive associative reflexive with_identities () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]} -defined {a} -valued Function-like non empty total V18({[a,a]},{a}) finite Element of bool [:{[a,a]},{a}:]

[:{[a,a]},{a}:] is finite set

bool [:{[a,a]},{a}:] is finite V40() set

Extract C is Element of {C}

(C,C) :-> C is Relation-like [:{C},{C}:] -defined {C} -valued Function-like total V18([:{C},{C}:],{C}) finite Element of bool [:[:{C},{C}:],{C}:]

[:{C},{C}:] is finite set

[:[:{C},{C}:],{C}:] is finite set

bool [:[:{C},{C}:],{C}:] is finite V40() set

[C,C] is set

{[C,C]} is Function-like non empty trivial finite 1 -element set

{[C,C]} --> C is Relation-like {[C,C]} -defined {C} -valued Function-like non empty total V18({[C,C]},{C}) finite Element of bool [:{[C,C]},{C}:]

[:{[C,C]},{C}:] is finite set

bool [:{[C,C]},{C}:] is finite V40() set

(C,C) :-> a is Relation-like [:{C},{C}:] -defined {a} -valued Function-like total V18([:{C},{C}:],{a}) finite Element of bool [:[:{C},{C}:],{a}:]

[:[:{C},{C}:],{a}:] is finite set

bool [:[:{C},{C}:],{a}:] is finite V40() set

{[C,C]} --> a is Relation-like {[C,C]} -defined {a} -valued Function-like non empty total V18({[C,C]},{a}) finite Element of bool [:{[C,C]},{a}:]

[:{[C,C]},{a}:] is finite set

bool [:{[C,C]},{a}:] is finite V40() set

({C},{a},(a :-> C),(a :-> C),((a,a) :-> a),(Extract C),((C,C) :-> C),((C,C) :-> a),((C,C) :-> a)) is () ()

the carrier of (C,a) is non empty trivial finite 1 -element set

c is Element of the carrier of (C,a)

b is Element of the carrier of (C,a)

C is set

a is set

(C,a) is non empty trivial finite non void 1 -element V57() trivial' Category-like transitive associative reflexive with_identities () ()

{C} is non empty trivial finite 1 -element set

{a} is non empty trivial finite 1 -element set

a :-> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

[:{a},{C}:] is finite set

bool [:{a},{C}:] is finite V40() set

{a} --> C is Relation-like {a} -defined {C} -valued Function-like non empty total V18({a},{C}) finite Element of bool [:{a},{C}:]

(a,a) :-> a is Relation-like [:{a},{a}:] -defined {a} -valued Function-like total V18([:{a},{a}:],{a}) finite Element of bool [:[:{a},{a}:],{a}:]

[:{a},{a}:] is finite set

[:[:{a},{a}:],{a}:] is finite set

bool [:[:{a},{a}:],{a}:] is finite V40() set

[a,a] is set

{[a,a]} is Function-like non empty trivial finite 1 -element set

{[a,a]} --> a is Relation-like {[a,a]