:: CAT_1 semantic presentation

K126() is Element of bool K122()
K122() is set
bool K122() is set
K47() is set
bool K47() is set
bool K126() is set

1 is non empty set

{1} is non empty trivial set

bool is set

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

bool [:[:{1},{1}:],{1}:] is set
[1,1] is non empty set
{1,1} is non empty set
{{1,1},{1}} is non empty set

{[1,1]} --> 1 is Relation-like {[1,1]} -defined {1} -valued Function-like non empty total V25({[1,1]},{1}) Element of bool [:{[1,1]},{1}:]
[:{[1,1]},{1}:] is Relation-like set
bool [:{[1,1]},{1}:] is set
(,{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1)) is () ()
C is ()
the carrier' of C is set
T is Element of the carrier' of C
D is Element of the carrier' of C
[T,D] is non empty set
{T,D} is non empty set
{T} is non empty trivial set
{{T,D},{T}} 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 Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is Relation-like set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
dom the of C is Relation-like set
the of C . (T,D) is set
the of C . [T,D] is set
C is non empty non void V59() ()
the carrier of C is non empty set
the carrier' of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
bool the carrier' of C is set
c9 is set
f1 is Element of the carrier' of C
dom f1 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . f1 is Element of the carrier of C
cod f1 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f1 is Element of the carrier of C
C is non empty non void V59() ()
the carrier' of C is non empty set
the carrier of C is non empty set
D is Element of the carrier' of C
dom D 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . D is Element of the carrier of C
cod D 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . D is Element of the carrier of C
T is Element of the carrier of C
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
c9 is Element of the carrier' of C
dom c9 is Element of the carrier of C
the Source of C . c9 is Element of the carrier of C
cod c9 is Element of the carrier of C
the Target of C . c9 is Element of the carrier of C
C is non empty non void V59() ()
the carrier' of C is non empty set
D is Element of the carrier' of C
dom D is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . D is Element of the carrier of C
cod D 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . D is Element of the carrier of C
(C,(dom D),(cod D)) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = dom D & cod b1 = cod D ) } is set
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
C is non empty non void V59() ()
the carrier' of C is non empty set
D is Element of the carrier' of C
dom D is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . D is Element of the carrier of C
cod D 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . D is Element of the carrier of C
(C,(dom D),(cod D)) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = dom D & cod b1 = cod D ) } is set
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . c 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 V25( 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
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
c9 is Element of the carrier of C
(C,c,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } is set
f1 is (C,D,T)
f2 is (C,c,c9)
dom f1 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . f1 is Element of the carrier of C
cod f1 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f1 is Element of the carrier of C
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
{c} is non empty trivial set
c9 is (C,D,T)
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
{c} is non empty trivial set
c9 is set
f1 is Element of the carrier' of C
dom f1 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . f1 is Element of the carrier of C
cod f1 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f1 is Element of the carrier of C
C is non empty non void V59() ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
c9 is Element of the carrier of C
(C,c,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } is set
f1 is (C,D,T)
{f1} is non empty trivial set

dom f2 is set
rng f2 is set
f2 . f1 is set
{(f2 . f1)} is non empty trivial set
C is set
{C} is non empty trivial set
D is set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
C is set
D is set
(C,D) is () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
C is non empty non void V59() ()
the carrier' of C is non empty set
T is Element of the carrier' of C
dom T is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . T is Element of the carrier of C
D is Element of the carrier' of C
cod D 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . D is Element of the carrier of C
(C,D,T) is Element of the carrier' of C
dom (C,D,T) is Element of the carrier of C
the Source of C . (C,D,T) is Element of the carrier of C
dom D is Element of the carrier of C
the Source of C . D is Element of the carrier of C
cod (C,D,T) is Element of the carrier of C
the Target of C . (C,D,T) is Element of the carrier of C
cod T is Element of the carrier of C
the Target of C . T is Element of the carrier of C
the carrier of C is non empty set
D is Element of the carrier of C
(C,D,D) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
the Element of the carrier' of C is Element of the carrier' of C
cod the Element of the carrier' of 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Target of C . the Element of the carrier' of C is Element of the carrier of C
dom the Element of the carrier' of 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Source of C . the Element of the carrier' of C is Element of the carrier of C
C is non empty non void V59() ()
the carrier' of C is non empty set
c is Element of the carrier' of C
dom c is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . c is Element of the carrier of C
T is Element of the carrier' of C
cod T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . T is Element of the carrier of C
dom T is Element of the carrier of C
the Source of C . T is Element of the carrier of C
D is Element of the carrier' of C
cod D is Element of the carrier of C
the Target of C . D is Element of the carrier of C
(C,D,T) is Element of the carrier' of C
(C,(C,D,T),c) is Element of the carrier' of C
(C,T,c) is Element of the carrier' of C
(C,D,(C,T,c)) is Element of the carrier' of C
the carrier of C is non empty set
D is Element of the carrier of C
the (C,D,D) is (C,D,D)
T is (C,D,D)
c is Element of the carrier of C
(C,D,c) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
(C,c,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = D ) } is set
c9 is (C,D,c)
(C,T,c9) is Element of the carrier' of C
c9 is (C,c,D)
(C,c9,T) is Element of the carrier' of C
C is set
D is set
(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
the carrier' of (C,D) is non empty trivial set
c is Element of the carrier' of (C,D)
T is Element of the carrier' of (C,D)
[c,T] is non empty set
{c,T} is non empty set
{c} is non empty trivial set
{{c,T},{c}} is non empty set
the of (C,D) is Relation-like [: the carrier' of (C,D), the carrier' of (C,D):] -defined the carrier' of (C,D) -valued Function-like Element of bool [:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):]
[: the carrier' of (C,D), the carrier' of (C,D):] is Relation-like set
[:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):] is Relation-like set
bool [:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):] is set
dom the of (C,D) is Relation-like set
dom c is Element of the carrier of (C,D)
the carrier of (C,D) is non empty trivial V35() set
the Source of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]
[: the carrier' of (C,D), the carrier of (C,D):] is Relation-like set
bool [: the carrier' of (C,D), the carrier of (C,D):] is set
the Source of (C,D) . c is Element of the carrier of (C,D)
cod T is Element of the carrier of (C,D)
the Target of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]
the Target of (C,D) . T is Element of the carrier of (C,D)

(0,0) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

[0,0] is non empty set
{0,0} is functional non empty set
is non empty set

(,,(),(),((0,0) :-> 0)) is () ()
C is non empty non void V59() () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D,D) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V59() () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is (C,D,D)
c is (C,D,D)
(C,D,D) is non empty Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
(C,c,T) is Element of the carrier' of C
C is set
D is set
(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
the carrier of (C,D) is non empty trivial V35() set
the carrier' of (C,D) is non empty trivial set
T is Element of the carrier of (C,D)
c is Element of the carrier of (C,D)
((C,D),T,c) is Element of bool the carrier' of (C,D)
bool the carrier' of (C,D) is set
{ b1 where b1 is Element of the carrier' of (C,D) : ( dom b1 = T & cod b1 = c ) } is set
c9 is Element of the carrier' of (C,D)
dom c9 is Element of the carrier of (C,D)
the Source of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]
[: the carrier' of (C,D), the carrier of (C,D):] is Relation-like set
bool [: the carrier' of (C,D), the carrier of (C,D):] is set
the Source of (C,D) . c9 is Element of the carrier of (C,D)
cod c9 is Element of the carrier of (C,D)
the Target of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]
the Target of (C,D) . c9 is Element of the carrier of (C,D)
C is set
D is set
(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
the carrier of (C,D) is non empty trivial V35() set
the carrier' of (C,D) is non empty trivial set
T is Element of the carrier of (C,D)
c is Element of the carrier of (C,D)
c9 is Element of the carrier' of (C,D)
((C,D),T,c) is Element of bool the carrier' of (C,D)
bool the carrier' of (C,D) is set
{ b1 where b1 is Element of the carrier' of (C,D) : ( dom b1 = T & cod b1 = c ) } is set
C is set
D is set
(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
the carrier of (C,D) is non empty trivial V35() set
T is Element of the carrier of (C,D)
c is Element of the carrier of (C,D)
((C,D),T,c) is Element of bool the carrier' of (C,D)
the carrier' of (C,D) is non empty trivial set
bool the carrier' of (C,D) is set
{ b1 where b1 is Element of the carrier' of (C,D) : ( dom b1 = T & cod b1 = c ) } is set
C is set
D is set
(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()
{C} is non empty trivial set
{D} is non empty trivial set

bool [:{D},{C}:] is set

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

bool [:[:{D},{D}:],{D}:] is set
[D,D] is non empty set
{D,D} is non empty set
{{D,D},{D}} is non empty set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like set
bool [:{[D,D]},{D}:] is set
({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()
the carrier of (C,D) is non empty trivial V35() set
T is Element of the carrier of (C,D)
c is Element of the carrier of (C,D)
c9 is Element of the carrier of (C,D)
f1 is Element of the carrier of (C,D)
f2 is ((C,D),T,c)
f is ((C,D),c9,f1)
C is non empty non void V59() () () () () () ()
the carrier' of C is non empty set
c is non empty non void V59() () () () () () ()
the carrier' of c is non empty set
D is Element of the carrier' of C
dom D is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . D is Element of the carrier of C
T is Element of the carrier' of C
cod T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . T is Element of the carrier of C
[D,T] is non empty set
{D,T} is non empty set
{D} is non empty trivial set
{{D,T},{D}} 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 Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is Relation-like set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
dom the of C is Relation-like set
c9 is Element of the carrier' of c
f1 is Element of the carrier' of c
[c9,f1] is non empty set
{c9,f1} is non empty set
{c9} is non empty trivial set
{{c9,f1},{c9}} 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 Element of bool [:[: the carrier' of c, the carrier' of c:], the carrier' of c:]
[: the carrier' of c, the carrier' of c:] is Relation-like set
[:[: the carrier' of c, the carrier' of c:], the carrier' of c:] is Relation-like set
bool [:[: the carrier' of c, the carrier' of c:], the carrier' of c:] is set
dom the of c is Relation-like set
dom c9 is Element of the carrier of c
the carrier of c is non empty set
the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of c, the carrier of c:] is set
the Source of c . c9 is Element of the carrier of c
cod f1 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 V25( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]
the Target of c . f1 is Element of the carrier of c
C is non empty non void V59() () () () () () ()
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 Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]
[: the carrier' of C, the carrier' of C:] is Relation-like set
[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set
bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is set
D is Element of the carrier' of C
dom D is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . D is Element of the carrier of C
T is Element of the carrier' of C
cod T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . T is Element of the carrier of C
(C,T,D) is Element of the carrier' of C
the of C . (D,T) is set
[D,T] is non empty set
{D,T} is non empty set
{D} is non empty trivial set
{{D,T},{D}} is non empty set
the of C . [D,T] is set
dom the of C is Relation-like set
C is non empty non void V59() () () () () () ()
the carrier' of C is non empty set
T is Element of the carrier' of C
dom T is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . T is Element of the carrier of C
D is Element of the carrier' of C
cod D 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . D is Element of the carrier of C
(C,D,T) is Element of the carrier' of C
dom (C,D,T) is Element of the carrier of C
the Source of C . (C,D,T) is Element of the carrier of C
dom D is Element of the carrier of C
the Source of C . D is Element of the carrier of C
cod (C,D,T) is Element of the carrier of C
the Target of C . (C,D,T) is Element of the carrier of C
cod T is Element of the carrier of C
the Target of C . T is Element of the carrier of C
C is non empty non void V59() () () () () () ()
the carrier' of C is non empty set
c is Element of the carrier' of C
dom c is Element of the carrier of C
the carrier of C is non empty set
the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . c is Element of the carrier of C
T is Element of the carrier' of C
cod T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . T is Element of the carrier of C
dom T is Element of the carrier of C
the Source of C . T is Element of the carrier of C
D is Element of the carrier' of C
cod D is Element of the carrier of C
the Target of C . D is Element of the carrier of C
(C,D,T) is Element of the carrier' of C
(C,(C,D,T),c) is Element of the carrier' of C
(C,T,c) is Element of the carrier' of C
(C,D,(C,T,c)) is Element of the carrier' of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
the carrier' of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier' of C
cod T 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Target of C . T is Element of the carrier of C
(C,T,(C,D)) is Element of the carrier' of C
dom T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Source of C . T is Element of the carrier of C
(C,(dom T),D) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = dom T & cod b1 = D ) } is set
c is (C, dom T,D)
(C,c,(C,D)) is Element of the carrier' of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
the carrier' of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier' of C
dom T 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . T is Element of the carrier of C
(C,(C,D),T) is Element of the carrier' of C
cod T 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . T is Element of the carrier of C
(C,D,(cod T)) is Element of bool the carrier' of C
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = cod T ) } is set
c is (C,D, cod T)
(C,(C,D),c) is Element of the carrier' of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
c9 is (C,D,T)
f1 is (C,T,c)
(C,c9,f1) is Element of the carrier' of C
cod c9 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Target of C . c9 is Element of the carrier of C
dom f1 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Source of C . f1 is Element of the carrier of C
cod f1 is Element of the carrier of C
the Target of C . f1 is Element of the carrier of C
cod (C,c9,f1) is Element of the carrier of C
the Target of C . (C,c9,f1) is Element of the carrier of C
dom c9 is Element of the carrier of C
the Source of C . c9 is Element of the carrier of C
dom (C,c9,f1) is Element of the carrier of C
the Source of C . (C,c9,f1) is Element of the carrier of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
c9 is (C,D,T)
f1 is (C,T,c)
(C,c9,f1) is Element of the carrier' of C
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
c9 is Element of the carrier of C
(C,c,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = c9 ) } is set
f1 is (C,D,T)
f2 is (C,T,c)
(C,D,T,c,f1,f2) is (C,D,c)
f is (C,c,c9)
(C,T,c,c9,f2,f) is (C,T,c9)
(C,D,T,c9,f1,(C,T,c,c9,f2,f)) is (C,D,c9)
(C,D,c,c9,(C,D,T,c,f1,f2),f) is (C,D,c9)
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
dom f 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 V25( 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 Relation-like set
bool [: the carrier' of C, the carrier of C:] is set
the Source of C . f is Element of the carrier of C
cod f2 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 V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
the Target of C . f2 is Element of the carrier of C
dom f2 is Element of the carrier of C
the Source of C . f2 is Element of the carrier of C
cod f1 is Element of the carrier of C
the Target of C . f1 is Element of the carrier of C
(C,T,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c9 ) } is set
c11 is Element of the carrier' of C
(C,c11,(C,T,c,c9,f2,f)) is Element of the carrier' of C
h is Element of the carrier' of C
c9 is Element of the carrier' of C
(C,h,c9) is Element of the carrier' of C
(C,c11,(C,h,c9)) is Element of the carrier' of C
(C,c11,h) is Element of the carrier' of C
(C,(C,c11,h),c9) is Element of the carrier' of C
(C,(C,D,T,c,f1,f2),c9) is Element of the carrier' of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
(C,D,D) is non empty Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T) is (C,T,T)
c is (C,D,T)
(C,D,T,T,c,(C,T)) is (C,D,T)
(C,c,(C,T)) is Element of the carrier' of C
(C,T,T) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = T ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
(C,D,D,T,(C,D),c) is (C,D,T)
(C,(C,D),c) is Element of the carrier' of C
(C,D,D) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D,D) is non empty Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
(C,D) is (C,D,D)
T is (C,D,D)
(C,D,D,D,(C,D),T) is (C,D,D)
(C,D,D,D,T,(C,D)) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
(C,D,D,D,(C,D),(C,D)) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
c9 is Element of the carrier of C
(C,c9,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c9 & cod b1 = D ) } is set
f1 is (C,c9,D)
(C,c9,D,T,f1,c) is (C,c9,T)
f2 is (C,c9,D)
(C,c9,D,T,f2,c) is (C,c9,T)
c9 is Element of the carrier of C
(C,c9,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c9 & cod b1 = D ) } is set
f1 is (C,c9,D)
(C,c9,D,T,f1,c) is (C,c9,T)
f2 is (C,c9,D)
(C,c9,D,T,f2,c) is (C,c9,T)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is Element of the carrier of C
c9 is (C,D,T)
f1 is (C,T,c)
(C,D,T,c,c9,f1) is (C,D,c)
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
f2 is Element of the carrier of C
(C,f2,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f2 & cod b1 = D ) } is set
f is (C,f2,D)
(C,f2,D,c,f,(C,D,T,c,c9,f1)) is (C,f2,c)
c9 is (C,f2,D)
(C,f2,D,c,c9,(C,D,T,c,c9,f1)) is (C,f2,c)
(C,f2,T) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f2 & cod b1 = T ) } is set
(C,f2,D,T,f,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,f,c9),f1) is (C,f2,c)
(C,f2,D,T,c9,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,c9,c9),f1) is (C,f2,c)
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
c9 is (C,D,T)
f1 is (C,T,c)
(C,D,T,c,c9,f1) is (C,D,c)
f2 is Element of the carrier of C
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
(C,f2,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f2 & cod b1 = D ) } is set
f is (C,f2,D)
(C,f2,D,T,f,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,f,c9),f1) is (C,f2,c)
(C,f2,D,c,f,(C,D,T,c,c9,f1)) is (C,f2,c)
c9 is (C,f2,D)
(C,f2,D,T,c9,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,c9,c9),f1) is (C,f2,c)
(C,f2,D,c,c9,(C,D,T,c,c9,f1)) is (C,f2,c)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
(C,T) is (C,T,T)
c is (C,D,T)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
f1 is Element of the carrier of C
(C,f1,T) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f1 & cod b1 = T ) } is set
f2 is (C,f1,T)
(C,f1,T,D,f2,c9) is (C,f1,D)
f is (C,f1,T)
(C,f1,T,D,f,c9) is (C,f1,D)
(C,f1,T,T,f2,(C,T,D,T,c9,c)) is (C,f1,T)
(C,f1,D,T,(C,f1,T,D,f,c9),c) is (C,f1,T)
(C,f1,T,T,f,(C,T,D,T,c9,c)) is (C,f1,T)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier of C
(C,T,D) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
c is (C,T,D)
(C,T,D,D,c,(C,D)) is (C,T,D)
c9 is (C,T,D)
(C,T,D,D,c9,(C,D)) is (C,T,D)
(C,D,D) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
c9 is Element of the carrier of C
(C,T,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c9 ) } is set
f1 is (C,T,c9)
(C,D,T,c9,c,f1) is (C,D,c9)
f2 is (C,T,c9)
(C,D,T,c9,c,f2) is (C,D,c9)
c9 is Element of the carrier of C
(C,T,c9) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c9 ) } is set
f1 is (C,T,c9)
(C,D,T,c9,c,f1) is (C,D,c9)
f2 is (C,T,c9)
(C,D,T,c9,c,f2) is (C,D,c9)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is Element of the carrier of C
c9 is (C,D,T)
f1 is (C,T,c)
(C,D,T,c,c9,f1) is (C,D,c)
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
f2 is Element of the carrier of C
(C,c,f2) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = f2 ) } is set
f is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),f) is (C,D,f2)
c9 is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),c9) is (C,D,f2)
(C,T,f2) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = f2 ) } is set
(C,T,c,f2,f1,f) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,f)) is (C,D,f2)
(C,T,c,f2,f1,c9) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,c9)) is (C,D,f2)
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
c9 is (C,D,T)
f1 is (C,T,c)
(C,D,T,c,c9,f1) is (C,D,c)
f2 is Element of the carrier of C
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
(C,c,f2) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = f2 ) } is set
f is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),f) is (C,D,f2)
(C,T,c,f2,f1,f) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,f)) is (C,D,f2)
c9 is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),c9) is (C,D,f2)
(C,T,c,f2,f1,c9) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,c9)) is (C,D,f2)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
(C,T) is (C,T,T)
c is (C,D,T)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
f1 is Element of the carrier of C
(C,T,f1) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = f1 ) } is set
f2 is (C,T,f1)
(C,D,T,f1,c,f2) is (C,D,f1)
f is (C,T,f1)
(C,D,T,f1,c,f) is (C,D,f1)
(C,T,T,f1,(C,T,D,T,c9,c),f2) is (C,T,f1)
(C,T,D,f1,c9,(C,D,T,f1,c,f)) is (C,T,f1)
(C,T,T,f1,(C,T,D,T,c9,c),f) is (C,T,f1)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
c is (C,D,T)
(C,D,D,T,(C,D),c) is (C,D,T)
c9 is (C,D,T)
(C,D,D,T,(C,D),c9) is (C,D,T)
(C,D,D) is non empty Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
(C,T) is (C,T,T)
c is (C,D,T)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
(C,D,T,D,c,c9) is (C,D,D)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
(C,D,T,D,c,c9) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
T is Element of the carrier of C
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
(C,T) is (C,T,T)
c is (C,D,T)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
f1 is (C,T,D)
(C,D,T,D,c,f1) is (C,D,D)
(C,T,D,D,c9,(C,D,T,D,c,f1)) is (C,T,D)
(C,T,T,D,(C,T),f1) is (C,T,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is (C,D,T)
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T) is (C,T,T)
(C,D) is (C,D,D)
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
(C,D,T,D,c,c9) is (C,D,D)
f1 is (C,T,D)
(C,T,D,T,f1,c) is (C,T,T)
(C,D,T,D,c,f1) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is (C,D,T)
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T) is (C,T,T)
(C,D) is (C,D,D)
c9 is (C,T,D)
(C,T,D,T,c9,c) is (C,T,T)
(C,D,T,D,c,c9) is (C,D,D)
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
f1 is Element of the carrier of C
(C,f1,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = f1 & cod b1 = D ) } is set
f2 is (C,f1,D)
(C,f1,D,T,f2,c) is (C,f1,T)
f is (C,f1,D)
(C,f1,D,T,f,c) is (C,f1,T)
(C,f1,D,D,f2,(C,D,T,D,c,c9)) is (C,f1,D)
(C,f1,T,D,(C,f1,D,T,f,c),c9) is (C,f1,D)
(C,f1,D,D,f,(C,D)) is (C,f1,D)
f1 is Element of the carrier of C
(C,T,f1) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = f1 ) } is set
f2 is (C,T,f1)
(C,D,T,f1,c,f2) is (C,D,f1)
f is (C,T,f1)
(C,D,T,f1,c,f) is (C,D,f1)
(C,T,T,f1,(C,T,D,T,c9,c),f2) is (C,T,f1)
(C,T,D,f1,c9,(C,D,T,f1,c,f)) is (C,T,f1)
(C,T,T,f1,(C,T),f) is (C,T,f1)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
(C,D) is (C,D,D)
(C,D,D) is non empty Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = D ) } is set
(C,D,D,D,(C,D),(C,D)) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is Element of the carrier of C
c9 is (C,D,T)
f1 is (C,T,c)
(C,D,T,c,c9,f1) is (C,D,c)
(C,D,T) is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is set
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = D ) } is set
(C,T) is (C,T,T)
(C,D) is (C,D,D)
f2 is (C,T,D)
(C,T,D,T,f2,c9) is (C,T,T)
(C,D,T,D,c9,f2) is (C,D,D)
(C,T,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = T & cod b1 = c ) } is set
(C,c,T) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = T ) } is set
(C,c) is (C,c,c)
f is (C,c,T)
(C,c,T,c,f,f1) is (C,c,c)
(C,T,c,T,f1,f) is (C,T,T)
(C,c,D) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = c & cod b1 = D ) } is set
(C,c,T,D,f,f2) is (C,c,D)
c9 is (C,c,D)
(C,c,D,c,c9,(C,D,T,c,c9,f1)) is (C,c,c)
(C,c,D,T,(C,c,T,D,f,f2),c9) is (C,c,T)
(C,c,T,c,(C,c,D,T,(C,c,T,D,f,f2),c9),f1) is (C,c,c)
(C,c,T,T,f,(C,T)) is (C,c,T)
(C,c,T,c,(C,c,T,T,f,(C,T)),f1) is (C,c,c)
(C,D,c) is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : ( dom b1 = D & cod b1 = c ) } is set
(C,D,c,D,(C,D,T,c,c9,f1),c9) is (C,D,D)
(C,D,c,T,(C,D,T,c,c9,f1),f) is (C,D,T)
(C,D,T,D,(C,D,c,T,(C,D,T,c,c9,f1),f),f2) is (C,D,D)
(C,D,T,T,c9,(C,T)) is (C,D,T)
(C,D,T,D,(C,D,T,T,c9,(C,T)),f2) is (C,D,D)
c9 is (C,c,D)
(C,c,D,c,c9,(C,D,T,c,c9,f1)) is (C,c,c)
(C,D,c,D,(C,D,T,c,c9,f1),c9) is (C,D,D)
C is non empty non void V59() () () () () () ()
the carrier of C is non empty set
D is Element of the carrier of C
T is Element of the carrier of C
c is (C,D,T)
(C,D,T,c) is (C,T,D)
(C,T,D,T,(C,D,T,c),c) is (C,T,T)
(C,T) is (C,T,T)
(C,D,T) is Element of bool the carrier' of C<