:: 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
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
1 is non empty set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Element of K126()
{0} is functional non empty trivial set
{1} is non empty trivial set
1 :-> 0 is Relation-like {1} -defined {0} -valued Function-like non empty total V25({1},{0}) Element of bool [:{1},{0}:]
[:{1},{0}:] is Relation-like set
bool [:{1},{0}:] is set
{1} --> 0 is Relation-like {1} -defined {0} -valued Function-like non empty total V25({1},{0}) Element of bool [:{1},{0}:]
(1,1) :-> 1 is Relation-like [:{1},{1}:] -defined {1} -valued Function-like total V25([:{1},{1}:],{1}) Element of bool [:[:{1},{1}:],{1}:]
[:{1},{1}:] is Relation-like set
[:[:{1},{1}:],{1}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
({0},{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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = c9 ) } is set
f1 is (C,D,T)
{f1} is non empty trivial set
f2 is Relation-like Function-like 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = c ) } is set
(C,c,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Element of K126()
(0,0) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()
{0} is functional non empty trivial set
0 :-> 0 is Relation-like {0} -defined {0} -valued Function-like non empty total V25({0},{0}) Element of bool [:{0},{0}:]
[:{0},{0}:] is Relation-like set
bool [:{0},{0}:] is set
{0} --> 0 is Relation-like {0} -defined {0} -valued Function-like non empty total V25({0},{0}) Element of bool [:{0},{0}:]
(0,0) :-> 0 is Relation-like [:{0},{0}:] -defined {0} -valued Function-like total V25([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]
[:[:{0},{0}:],{0}:] is Relation-like set
bool [:[:{0},{0}:],{0}:] is set
[0,0] is non empty set
{0,0} is functional non empty set
{{0,0},{0}} is non empty set
{[0,0]} is Relation-like Function-like constant non empty trivial set
{[0,0]} --> 0 is Relation-like {[0,0]} -defined {0} -valued Function-like non empty total V25({[0,0]},{0}) Element of bool [:{[0,0]},{0}:]
[:{[0,0]},{0}:] is Relation-like set
bool [:{[0,0]},{0}:] is set
({0},{0},(0 :-> 0),(0 :-> 0),((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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
{ b₁ where b₁ is Element of the carrier' of (C,D) : ( dom b₁ = T & cod b₁ = 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
{ b₁ where b₁ is Element of the carrier' of (C,D) : ( dom b₁ = T & cod b₁ = 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
{ b₁ where b₁ is Element of the carrier' of (C,D) : ( dom b₁ = T & cod b₁ = 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
D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
[:{D},{C}:] is Relation-like set
bool [:{D},{C}:] is set
{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]
(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]
[:{D},{D}:] is Relation-like set
[:[:{D},{D}:],{D}:] is Relation-like set
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]} is Relation-like Function-like constant non empty trivial 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = dom T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
(C,D,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
(C,D,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
c9 is Element of the carrier of C
(C,c,c9) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c9 ) } is set
c₁₁ is Element of the carrier' of C
(C,c₁₁,(C,T,c,c9,f2,f)) is Element of the carrier' of C
h is Element of the carrier' of C
c₉ is Element of the carrier' of C
(C,h,c₉) is Element of the carrier' of C
(C,c₁₁,(C,h,c₉)) is Element of the carrier' of C
(C,c₁₁,h) is Element of the carrier' of C
(C,(C,c₁₁,h),c₉) is Element of the carrier' of C
(C,(C,D,T,c,f1,f2),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
(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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c9 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c9 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
f2 is Element of the carrier of C
(C,f2,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f2 & cod b₁ = D ) } is set
f is (C,f2,D)
(C,f2,D,c,f,(C,D,T,c,c9,f1)) is (C,f2,c)
c₉ is (C,f2,D)
(C,f2,D,c,c₉,(C,D,T,c,c9,f1)) is (C,f2,c)
(C,f2,T) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f2 & cod b₁ = 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,c₉,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,c₉,c9),f1) is (C,f2,c)
(C,D,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = c ) } is set
(C,f2,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f2 & cod b₁ = 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)
c₉ is (C,f2,D)
(C,f2,D,T,c₉,c9) is (C,f2,T)
(C,f2,T,c,(C,f2,D,T,c₉,c9),f1) is (C,f2,c)
(C,f2,D,c,c₉,(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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f1 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
f2 is Element of the carrier of C
(C,c,f2) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = f2 ) } is set
f is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),f) is (C,D,f2)
c₉ is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),c₉) is (C,D,f2)
(C,T,f2) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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,c₉) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,c₉)) is (C,D,f2)
(C,D,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
c is Element of the carrier of C
(C,T,c) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = c ) } is set
(C,c,f2) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = 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)
c₉ is (C,c,f2)
(C,D,c,f2,(C,D,T,c,c9,f1),c₉) is (C,D,f2)
(C,T,c,f2,f1,c₉) is (C,T,f2)
(C,D,T,f2,c9,(C,T,c,f2,f1,c₉)) 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = D ) } is set
f1 is Element of the carrier of C
(C,f1,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = f1 & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = T ) } is set
(C,T,D) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = T & cod b₁ = c ) } is set
(C,c,T) is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = 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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = c & cod b₁ = D ) } is set
(C,c,T,D,f,f2) is (C,c,D)
c₉ is (C,c,D)
(C,c,D,c,c₉,(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
{ b₁ where b₁ is Element of the carrier' of C : ( dom b₁ = D & cod b₁ = c ) } is set
(C,D,c,D,(C,D,T,c,c9,f1),c₉) 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)
c₉ is (C,c,D)
(C,c,D,c,c₉,(C,D,T,c,c9,f1)) is (C,c,c)
(C,D,c,D,(C,D,T,c,c9,f1),c₉) 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<