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