:: CAT_2  semantic presentation begin  
theorem :: CAT_2:1 canceled; 
 
theorem :: CAT_2:2 canceled; 
 
theorem :: CAT_2:3 canceled; 
 
theorem :: CAT_2:4 canceled; 
 






definitionlet "B", "C" be   ($#l1_cat_1 :::"Category":::); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "B" :::"-->"::: "c" ->    ($#m2_cat_1 :::"Functor"::: )   "of" "B" "," "C" equals :: CAT_2:def 1 (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "B")  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  "c" ")" )); end; 







:: deftheorem    defines :::"-->"::: CAT_2:def 1 :  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "B"))  ($#k1_cat_2 :::"-->"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "B")))  ($#k8_funcop_1 :::"-->"::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" ))))); 
 
theorem :: CAT_2:5 (Bool  "for" (Set (Var "C")) "," (Set (Var "B")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "(" (Set (Var "B"))  ($#k1_cat_2 :::"-->"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "c")))))) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); func  :::"Funct":::  "(" "C" "," "D" ")"  ->    ($#m1_hidden :::"set"::: )   means :: CAT_2:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" "C" "," "D")  ")" )); end; 






:: deftheorem    defines :::"Funct"::: CAT_2:def 2 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cat_2 :::"Funct"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D")))  ")" ))  ")" ))); 
 registrationlet "C", "D" be   ($#l1_cat_1 :::"Category":::); 
cluster (Set   ($#k2_cat_2 :::"Funct"::: )   "(" "C" "," "D" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); mode  :::"FUNCTOR-DOMAIN":::  "of" "C" "," "D" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   means :: CAT_2:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" it "holds"  (Bool (Set (Var "x")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" "C" "," "D")); end; 






:: deftheorem    defines :::"FUNCTOR-DOMAIN"::: CAT_2:def 3 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "b3")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_cat_2 :::"FUNCTOR-DOMAIN"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "b3")) "holds"  (Bool (Set (Var "x")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))))  ")" ))); 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m1_cat_2 :::"FUNCTOR-DOMAIN"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "F" ->    ($#m2_cat_1 :::"Functor"::: )   "of" "C" "," "D"; end; definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "C", "D" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m1_cat_2 :::"FUNCTOR-DOMAIN"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); let "T" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "F")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); :: original: :::"."::: redefine func "T" :::"."::: "x" ->    ($#m2_cat_2 :::"Element"::: )   "of" "F"; end; definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); :: original: :::"Funct"::: redefine func  :::"Funct":::  "(" "C" "," "D" ")"  ->    ($#m1_cat_2 :::"FUNCTOR-DOMAIN"::: )   "of" "C" "," "D"; end; definitionlet "C" be   ($#l1_cat_1 :::"Category":::); mode  :::"Subcategory":::  "of" "C" ->   ($#l1_cat_1 :::"Category":::) means :: CAT_2:def 4 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C")) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" it  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Object":::) "of" "C"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" )))  ")" ) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" it)  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" "C")) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" it  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Object":::) "of" "C"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a9")))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Subcategory"::: CAT_2:def 4 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "b2")) "being"   ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "b2"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" )))  ")" ) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "b2")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "b2"))  (Bool  "for" (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a9")))))  ")" )  ")" )  ")" )); 
 registrationlet "C" be   ($#l1_cat_1 :::"Category":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  bbbadV14_STRUCT_0()   ($#v1_cat_1 :::"strict"::: )     ($#v2_cat_1 :::"Category-like"::: )     ($#v3_cat_1 :::"transitive"::: )     ($#v4_cat_1 :::"associative"::: )     ($#v5_cat_1 :::"reflexive"::: )     ($#v6_cat_1 :::"with_identities"::: )    for    ($#m3_cat_2 :::"Subcategory"::: )   "of" "C"; 
end; 



theorem :: CAT_2:6 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Var "e")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")))))) ; 
 
theorem :: CAT_2:7 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "E")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C")))))) ; 
 
theorem :: CAT_2:8 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")))))) ; 
 
theorem :: CAT_2:9 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "f9")))) "holds"  (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f9")))) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f9"))))  ")" ))))) ; 
 
theorem :: CAT_2:10 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9"))) & (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "f")) "is"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set (Var "a9")) "," (Set (Var "b9")))))))) ; 
 
theorem :: CAT_2:11 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "f9")) "," (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "f9"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "g9"))) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g9"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f9")))))))) ; 
 
theorem :: CAT_2:12 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set (Var "C")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")))) ; 
 
theorem :: CAT_2:13 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k10_cat_1 :::"id"::: )  (Set (Var "E"))) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "E")) "," (Set (Var "C"))))) ; 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "E" be    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Const "C")); func  :::"incl"::: "E" ->    ($#m2_cat_1 :::"Functor"::: )   "of" "E" "," "C" equals :: CAT_2:def 5 (Set   ($#k10_cat_1 :::"id"::: )  "E"); end; 






:: deftheorem    defines :::"incl"::: CAT_2:def 5 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k5_cat_2 :::"incl"::: )  (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_cat_1 :::"id"::: )  (Set (Var "E")))))); 
 
theorem :: CAT_2:14 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set (Var "E")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))))) ; 
 
theorem :: CAT_2:15 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set (Var "E")) ")" )  ($#k8_cat_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))))) ; 
 
theorem :: CAT_2:16 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k5_cat_2 :::"incl"::: )  (Set (Var "E"))) "is"   ($#v14_cat_1 :::"faithful"::: )  ))) ; 
 
theorem :: CAT_2:17 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k5_cat_2 :::"incl"::: )  (Set (Var "E"))) "is"   ($#v13_cat_1 :::"full"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" ))))  ")" ))) ; 
 definitionlet "D" be   ($#l1_cat_1 :::"Category":::); let "C" be    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Const "D")); attr "C" is  :::"full":::  means :: CAT_2:def 6 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#m1_subset_1 :::"Object":::) "of" "C"  (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_subset_1 :::"Object":::) "of" "D"  "st" (Bool (Bool (Set (Var "c1"))  ($#r1_hidden :::"="::: )  (Set (Var "d1"))) & (Bool (Set (Var "c2"))  ($#r1_hidden :::"="::: )  (Set (Var "d2")))) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )))); end; 





:: deftheorem    defines :::"full"::: CAT_2:def 6 :  (Bool  "for" (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v1_cat_2 :::"full"::: )  ) "iff" (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "c1"))  ($#r1_hidden :::"="::: )  (Set (Var "d1"))) & (Bool (Set (Var "c2"))  ($#r1_hidden :::"="::: )  (Set (Var "d2")))) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ))))  ")" ))); 
 registrationlet "D" be   ($#l1_cat_1 :::"Category":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  bbbadV14_STRUCT_0()   ($#v2_cat_1 :::"Category-like"::: )     ($#v3_cat_1 :::"transitive"::: )     ($#v4_cat_1 :::"associative"::: )     ($#v5_cat_1 :::"reflexive"::: )     ($#v6_cat_1 :::"with_identities"::: )     ($#v1_cat_2 :::"full"::: )    for    ($#m3_cat_2 :::"Subcategory"::: )   "of" "D"; 
end; 
theorem :: CAT_2:18 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "E")) "is"   ($#v1_cat_2 :::"full"::: )  ) "iff" (Bool (Set   ($#k5_cat_2 :::"incl"::: )  (Set (Var "E"))) "is"   ($#v13_cat_1 :::"full"::: )  )  ")" ))) ; 
 
theorem :: CAT_2:19 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "O")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) where a, b "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "O"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "O")))  ")" )  "}"  ) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C")))))) ; 
 
theorem :: CAT_2:20 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "O")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) where a, b "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "O"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "O")))  ")" )  "}"  ))) "holds"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "O"))) & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "O"))) & (Bool (Set (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C")))  ($#k1_realset1 :::"||"::: )  (Set (Var "M"))) "is"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "M")))  ")" )))) ; 
 registrationlet "O", "M" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "d", "c" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "M")) "," (Set (Const "O")); let "p" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "M")) "," (Set (Const "M")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "M")); 
cluster (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  "O" "," "M" "," "d" "," "c" "," "p" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  ; 
end; 
theorem :: CAT_2:21 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "O")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "O"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "M"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "O")) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) where a, b "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "O"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "O")))  ")" )  "}"  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C")))  ($#k1_realset1 :::"||"::: )  (Set (Var "M"))))) "holds"  (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set (Var "O")) "," (Set (Var "M")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "p")) "#)" ) "is"   ($#v1_cat_2 :::"full"::: )     ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))))))))) ; 
 
theorem :: CAT_2:22 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "O")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "O"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set (Var "O")) "," (Set (Var "M")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "p")) "#)" ) "is"   ($#v1_cat_2 :::"full"::: )     ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")))) "holds"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) where a, b "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "O"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "O")))  ")" )  "}"  )) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C")))  ($#k2_partfun1 :::"|"::: )  (Set (Var "M")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C")))  ($#k1_realset1 :::"||"::: )  (Set (Var "M"))))  ")" )))))) ; 
 definitionlet "X1", "X2", "Y1", "Y2" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f1" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "f2" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"[:"::: redefine func :::"[:":::"f1" "," "f2":::":]"::: ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) "X1" "," "X2" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) "Y1" "," "Y2" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "A", "B" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "A")); let "g" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "B")); :: original: :::"|:"::: redefine func :::"|:":::"f" "," "g":::":|"::: ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); func :::"[:":::"C" "," "D":::":]"::: ->   ($#l1_cat_1 :::"Category":::) equals :: CAT_2:def 7 (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "D") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "D") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "C") "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "D") ($#k6_cat_2 :::":]"::: ) ) "," (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "C") "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "D") ($#k6_cat_2 :::":]"::: ) ) "," (Set  ($#k7_cat_2 :::"|:"::: ) (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" "C") "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" "D") ($#k7_cat_2 :::":|"::: ) ) "#)" ); end; 






:: deftheorem    defines :::"[:"::: CAT_2:def 7 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "D"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "D"))) ($#k6_cat_2 :::":]"::: ) ) "," (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "D"))) ($#k6_cat_2 :::":]"::: ) ) "," (Set  ($#k7_cat_2 :::"|:"::: ) (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "D"))) ($#k7_cat_2 :::":|"::: ) ) "#)" ))); 
 
theorem :: CAT_2:23 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "D"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))  ($#r1_funct_2 :::"="::: )  (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "D"))) ($#k6_cat_2 :::":]"::: ) )) & (Bool (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))  ($#r1_funct_2 :::"="::: )  (Set  ($#k6_cat_2 :::"[:"::: ) (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "D"))) ($#k6_cat_2 :::":]"::: ) )) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_cat_2 :::"|:"::: ) (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "D"))) ($#k7_cat_2 :::":|"::: ) ))  ")" )) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "d" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "D")); :: original: :::"["::: redefine func :::"[":::"c" "," "d":::"]"::: ->   ($#m1_subset_1 :::"Object":::) "of" (Set  ($#k8_cat_2 :::"[:"::: ) "C" "," "D" ($#k8_cat_2 :::":]"::: ) ); end; 
theorem :: CAT_2:24 canceled; 
 
theorem :: CAT_2:25 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "cd")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ) (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Var "cd"))  ($#r1_hidden :::"="::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k9_cat_2 :::"]"::: ) )))))) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "f" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); let "g" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "D")); :: original: :::"["::: redefine func :::"[":::"f" "," "g":::"]"::: ->   ($#m1_subset_1 :::"Morphism":::) "of" (Set  ($#k8_cat_2 :::"[:"::: ) "C" "," "D" ($#k8_cat_2 :::":]"::: ) ); end; 
theorem :: CAT_2:26 canceled; 
 
theorem :: CAT_2:27 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "fg")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "D")) "st" (Bool (Set (Var "fg"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) )))))) ; 
 
theorem :: CAT_2:28 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")) ")" ) ($#k9_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")) ")" ) ($#k9_cat_2 :::"]"::: ) ))  ")" )))) ; 
 
theorem :: CAT_2:29 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "g")) "," (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f9")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g9")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f9")) "," (Set (Var "g9")) ($#k10_cat_2 :::"]"::: ) )  ($#k1_cat_1 :::"(*)"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set (Var "f9"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "g9"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "g")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))) ; 
 
theorem :: CAT_2:30 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "g")) "," (Set (Var "g9")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f9")) "," (Set (Var "g9")) ($#k10_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) )))) "holds"  (Bool (Set (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f9")) "," (Set (Var "g9")) ($#k10_cat_2 :::"]"::: ) )  ($#k1_cat_1 :::"(*)"::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set (Var "f9"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "g9"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "g")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))) ; 
 
theorem :: CAT_2:31 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k9_cat_2 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" ) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "d")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))) ; 
 
theorem :: CAT_2:32 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "," (Set (Var "d9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k9_cat_2 :::"]"::: ) ) "," (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c9")) "," (Set (Var "d9")) ($#k9_cat_2 :::"]"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")"  ")" ) "," (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "d")) "," (Set (Var "d9")) ")"  ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; 
 
theorem :: CAT_2:33 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set (Var "c")) "," (Set (Var "c9"))  (Bool  "for" (Set (Var "d")) "," (Set (Var "d9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "g")) "being"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set (Var "d")) "," (Set (Var "d9"))  "st" (Bool (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "d")) "," (Set (Var "d9")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ) "is"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k9_cat_2 :::"]"::: ) ) "," (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "c9")) "," (Set (Var "d9")) ($#k9_cat_2 :::"]"::: ) ))))))) ; 
 definitionlet "C", "C9", "D" be   ($#l1_cat_1 :::"Category":::); let "S" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "D")); let "m" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); let "m9" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C9")); :: original: :::"."::: redefine func "S" :::".":::  "(" "m" "," "m9" ")"  ->   ($#m1_subset_1 :::"Morphism":::) "of" "D"; end; 
theorem :: CAT_2:34 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "("  ($#k1_funct_5 :::"curry"::: )  (Set (Var "S")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" )) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C9")) "," (Set (Var "D")))))) ; 
 
theorem :: CAT_2:35 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set  "("  ($#k3_funct_5 :::"curry'"::: )  (Set (Var "S")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c9")) ")" )) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D")))))) ; 
 definitionlet "C", "C9", "D" be   ($#l1_cat_1 :::"Category":::); let "S" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "D")); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "S" :::"?-"::: "c" ->    ($#m2_cat_1 :::"Functor"::: )   "of" "C9" "," "D" equals :: CAT_2:def 8 (Set (Set  "("  ($#k1_funct_5 :::"curry"::: )  "S" ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  "c" ")" )); end; 









:: deftheorem    defines :::"?-"::: CAT_2:def 8 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "S"))  ($#k12_cat_2 :::"?-"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_funct_5 :::"curry"::: )  (Set (Var "S")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" )))))); 
 
theorem :: CAT_2:36 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set  "(" (Set (Var "S"))  ($#k12_cat_2 :::"?-"::: )  (Set (Var "c")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k11_cat_2 :::"."::: )   "(" (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" ) "," (Set (Var "f")) ")" )))))) ; 
 
theorem :: CAT_2:37 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "(" (Set (Var "S"))  ($#k12_cat_2 :::"?-"::: )  (Set (Var "c")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c9")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "S")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")" )))))) ; 
 definitionlet "C", "C9", "D" be   ($#l1_cat_1 :::"Category":::); let "S" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "D")); let "c9" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C9")); func "S" :::"-?"::: "c9" ->    ($#m2_cat_1 :::"Functor"::: )   "of" "C" "," "D" equals :: CAT_2:def 9 (Set (Set  "("  ($#k3_funct_5 :::"curry'"::: )  "S" ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  "c9" ")" )); end; 









:: deftheorem    defines :::"-?"::: CAT_2:def 9 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set (Var "S"))  ($#k13_cat_2 :::"-?"::: )  (Set (Var "c9")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_funct_5 :::"curry'"::: )  (Set (Var "S")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c9")) ")" )))))); 
 
theorem :: CAT_2:38 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "(" (Set (Var "S"))  ($#k13_cat_2 :::"-?"::: )  (Set (Var "c9")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k11_cat_2 :::"."::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c9")) ")" ) ")" )))))) ; 
 
theorem :: CAT_2:39 (Bool  "for" (Set (Var "C")) "," (Set (Var "C9")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "(" (Set (Var "S"))  ($#k13_cat_2 :::"-?"::: )  (Set (Var "c9")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "S")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")" )))))) ; 
 
theorem :: CAT_2:40 (Bool  "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "("  ($#k4_cat_2 :::"Funct"::: )   "(" (Set (Var "B")) "," (Set (Var "D")) ")"  ")" )  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "B"))) "," (Set  "("  ($#k4_cat_2 :::"Funct"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds"  (Bool (Set (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set (Var "b")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set (Var "c")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "b")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" ))))  ")" )) "holds"  (Bool  "ex" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D")) "st"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "S"))  ($#k11_cat_2 :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" ))))))))) ; 
 
theorem :: CAT_2:41 (Bool  "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "("  ($#k4_cat_2 :::"Funct"::: )   "(" (Set (Var "B")) "," (Set (Var "D")) ")"  ")" )  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "B"))) "," (Set  "("  ($#k4_cat_2 :::"Funct"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" )  "st" (Bool (Bool  "ex" (Set (Var "S")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "D")) "st"  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Set (Var "S"))  ($#k13_cat_2 :::"-?"::: )  (Set (Var "c")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set (Var "c")))) & (Bool (Set (Set (Var "S"))  ($#k12_cat_2 :::"?-"::: )  (Set (Var "b")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set (Var "b"))))  ")" ))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "M"))  ($#k3_cat_2 :::"."::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" )))))))) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); func  :::"pr1":::  "(" "C" "," "D" ")"  ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) "C" "," "D" ($#k8_cat_2 :::":]"::: ) ) "," "C" equals :: CAT_2:def 10 (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "D") ")" ); func  :::"pr2":::  "(" "C" "," "D" ")"  ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) "C" "," "D" ($#k8_cat_2 :::":]"::: ) ) "," "D" equals :: CAT_2:def 11 (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "D") ")" ); end; 












:: deftheorem    defines :::"pr1"::: CAT_2:def 10 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set   ($#k14_cat_2 :::"pr1"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) ")" ))); 
 
:: deftheorem    defines :::"pr2"::: CAT_2:def 11 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set   ($#k15_cat_2 :::"pr2"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) ")" ))); 
 
theorem :: CAT_2:42 canceled; 
 
theorem :: CAT_2:43 canceled; 
 
theorem :: CAT_2:44 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "("  ($#k14_cat_2 :::"pr1"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" ) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c")))))) ; 
 
theorem :: CAT_2:45 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  "("  ($#k15_cat_2 :::"pr2"::: )   "(" (Set (Var "C")) "," (Set (Var "D")) ")"  ")" ) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "d")))))) ; 
 definitionlet "C", "D", "D9" be   ($#l1_cat_1 :::"Category":::); let "T" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); let "T9" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D9")); :: original: :::"<:"::: redefine func :::"<:":::"T" "," "T9":::":>"::: ->    ($#m2_cat_1 :::"Functor"::: )   "of" "C" "," (Set  ($#k8_cat_2 :::"[:"::: ) "D" "," "D9" ($#k8_cat_2 :::":]"::: ) ); end; 
theorem :: CAT_2:46 canceled; 
 
theorem :: CAT_2:47 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "D9")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "T")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "T9")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D9"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  ($#k16_cat_2 :::"<:"::: ) (Set (Var "T")) "," (Set (Var "T9")) ($#k16_cat_2 :::":>"::: ) ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set  "(" (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "T9")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")) ")" ) ($#k9_cat_2 :::"]"::: ) )))))) ; 
 
theorem :: CAT_2:48 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "C9")) "," (Set (Var "D9")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "T")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "T9")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C9")) "," (Set (Var "D9")) "holds"  (Bool (Set  ($#k6_cat_2 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T9")) ($#k6_cat_2 :::":]"::: ) )  ($#r1_funct_2 :::"="::: )  (Set  ($#k16_cat_2 :::"<:"::: ) (Set  "(" (Set (Var "T"))  ($#k9_cat_1 :::"*"::: )  (Set  "("  ($#k14_cat_2 :::"pr1"::: )   "(" (Set (Var "C")) "," (Set (Var "C9")) ")"  ")" ) ")" ) "," (Set  "(" (Set (Var "T9"))  ($#k9_cat_1 :::"*"::: )  (Set  "("  ($#k15_cat_2 :::"pr2"::: )   "(" (Set (Var "C")) "," (Set (Var "C9")) ")"  ")" ) ")" ) ($#k16_cat_2 :::":>"::: ) ))))) ; 
 definitionlet "C", "C9", "D", "D9" be   ($#l1_cat_1 :::"Category":::); let "T" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); let "T9" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C9")) "," (Set (Const "D9")); :: original: :::"[:"::: redefine func :::"[:":::"T" "," "T9":::":]"::: ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set  ($#k8_cat_2 :::"[:"::: ) "C" "," "C9" ($#k8_cat_2 :::":]"::: ) ) "," (Set  ($#k8_cat_2 :::"[:"::: ) "D" "," "D9" ($#k8_cat_2 :::":]"::: ) ); end; 
theorem :: CAT_2:49 canceled; 
 
theorem :: CAT_2:50 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "C9")) "," (Set (Var "D9")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "T")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "T9")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C9")) "," (Set (Var "D9"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C9")) "holds"  (Bool (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set  ($#k17_cat_2 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T9")) ($#k17_cat_2 :::":]"::: ) ) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "c")) "," (Set (Var "c9")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k9_cat_2 :::"["::: ) (Set  "(" (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "T9")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c9")) ")" ) ($#k9_cat_2 :::"]"::: ) ))))))) ;