:: 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₁ where b₁ is Element of the carrier' of C : ( dom b₁ = a & cod b₁ = c ) } is set
Hom (c,a) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = a ) } is set
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₁ where b₁ is Element of the carrier' of C : ( dom b₁ = F9 & cod b₁ = b ) } is set
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₁ where b₁ is Element of the carrier' of C : ( dom b₁ = F9 & cod b₁ = g ) } is set
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₁ where b₁ is Element of the carrier' of C : ( dom b₁ = F9 & cod b₁ = cod i1 ) } is set
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]