:: CAT_5  semantic presentation begin  
theorem :: CAT_5:1 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_cat_1 :::"CatStr"::: )    "st" (Bool (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "D"))) "#)" ))) "holds"  (Bool  "("  (Bool (Set (Var "D")) "is"   ($#v2_cat_1 :::"Category-like"::: )  ) & (Bool (Set (Var "D")) "is"   ($#v3_cat_1 :::"transitive"::: )  ) & (Bool (Set (Var "D")) "is"   ($#v4_cat_1 :::"associative"::: )  ) & (Bool (Set (Var "D")) "is"   ($#v5_cat_1 :::"reflexive"::: )  ) & (Bool (Set (Var "D")) "is"   ($#v6_cat_1 :::"with_identities"::: )  )  ")" ))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_cat_1 :::"CatStr"::: )  ; attr "IT" is  :::"with_triple-like_morphisms":::  means :: CAT_5:def 1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "IT" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )))); end; 




:: deftheorem    defines :::"with_triple-like_morphisms"::: CAT_5:def 1 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_cat_1 :::"CatStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_cat_5 :::"with_triple-like_morphisms"::: )  ) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ))))  ")" )); 
 registration
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"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    for    ($#l1_cat_1 :::"CatStr"::: )  ; 
end; 
theorem :: CAT_5:2 (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_cat_5 :::"with_triple-like_morphisms"::: )     ($#l1_cat_1 :::"CatStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k13_mcart_1 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k14_mcart_1 :::"`12"::: )  )) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set  "(" (Set (Var "f"))  ($#k2_xtuple_0 :::"`2"::: )  ")" ) ($#k4_tarski :::"]"::: ) ))  ")" ))) ; 
 definitionlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_cat_5 :::"with_triple-like_morphisms"::: )     ($#l1_cat_1 :::"CatStr"::: )  ; let "f" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); :: original: :::"`11"::: redefine func "f" :::"`11":::  ->   ($#m1_subset_1 :::"Object":::) "of" "C"; :: original: :::"`12"::: redefine func "f" :::"`12":::  ->   ($#m1_subset_1 :::"Object":::) "of" "C"; end; scheme  :: CAT_5:sch 1 CatEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "C")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )(Bool  "ex" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set F3 "(" (Set (Var "f2")) "," (Set (Var "f1")) ")" ) ($#k4_tarski :::"]"::: ) ))))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))])) "holds"  (Bool  "("  (Bool (Set F3 "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "c")) "," (Set F3 "(" (Set (Var "g")) "," (Set (Var "f")) ")" )])  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "f"))]) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"   (Bool  "("   "("  (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g"))])) "implies" (Bool (Set F3 "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")"  &  "("  (Bool (Bool P1[(Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "g"))])) "implies" (Bool (Set F3 "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")"   ")" ))  ")" )  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))]) & (Bool P1[(Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "g"))]) & (Bool P1[(Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "h"))])) "holds"  (Bool (Set F3 "(" (Set (Var "h")) "," (Set F3 "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set F3 "(" (Set (Var "h")) "," (Set (Var "g")) ")" ) "," (Set (Var "f")) ")" ))))
 proof 


end; scheme  :: CAT_5:sch 2 CatUniq{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C1"))))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C1")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )(Bool  "ex" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C1"))  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set F3 "(" (Set (Var "f2")) "," (Set (Var "f1")) ")" ) ($#k4_tarski :::"]"::: ) ))))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])) "holds"  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C2"))))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C2")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )(Bool  "ex" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "f"))])  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C2"))  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k1_domain_1 :::"]"::: ) ) "," (Set F3 "(" (Set (Var "f2")) "," (Set (Var "f1")) ")" ) ($#k4_tarski :::"]"::: ) ))))  ")" )) "holds"  (Bool (Set (Var "C1"))  ($#r1_hidden :::"="::: )  (Set (Var "C2"))))
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool P1[(Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "f"))]) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"   (Bool  "("   "("  (Bool (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g"))])) "implies" (Bool (Set F3 "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")"  &  "("  (Bool (Bool P1[(Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "g"))])) "implies" (Bool (Set F3 "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")"   ")" ))  ")" )  ")" )))
 proof 


end; scheme  :: CAT_5:sch 3 FunctorEx{ F1() ->   ($#l1_cat_1 :::"Category":::), F2() ->   ($#l1_cat_1 :::"Category":::), F3(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Object":::) "of" (Set F2 "("  ")" ), F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "f")) ")" ))))
 provided
(Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool (Set F4 "(" (Set (Var "f")) ")" ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "f")) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ")" ))  ")" )  ")" )  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set F4 "(" (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "a")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_1 :::"id"::: )  (Set F3 "(" (Set (Var "a")) ")" ))))
 and  
(Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set F2 "("  ")" )  "st" (Bool (Bool (Set (Var "g1"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "f1")) ")" )) & (Bool (Set (Var "g2"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "f2")) ")" )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set F4 "(" (Set  "(" (Set (Var "f2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f1")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "g1"))))))
 proof 


end; 
theorem :: CAT_5:3 (Bool  "for" (Set (Var "C1")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "C2")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C1"))  "st" (Bool (Bool (Set (Var "C1")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C2")))) "holds"  (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C2"))) "#)" )))) ; 
 
theorem :: CAT_5:4 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "D")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Var "E")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")))))) ; 
 definitionlet "C1", "C2" be   ($#l1_cat_1 :::"Category":::); given "C" being   ($#l1_cat_1 :::"Category":::) such that 
(Bool (Set (Const "C1")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Const "C")))
 and  
(Bool (Set (Const "C2")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Const "C")))
 ; given "o1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C1")) such that 
(Bool (Set (Const "o1")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C2")))
 ; func "C1" :::"/\"::: "C2" ->   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) means :: CAT_5:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C1")  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C2"))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C1")  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C2"))) & (Bool (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "C1")  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C2"))) & (Bool (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "C1")  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C2"))) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" "C1")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C2")))  ")" ); end; 







:: deftheorem    defines :::"/\"::: CAT_5:def 2 :  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool  "ex" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::) "st"  (Bool  "("  (Bool (Set (Var "C1")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))) & (Bool (Set (Var "C2")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C")))  ")" )) & (Bool  "ex" (Set (Var "o1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C1")) "st" (Bool (Set (Var "o1")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C2"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C1"))  ($#k3_cat_5 :::"/\"::: )  (Set (Var "C2")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C1")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))))) & (Bool (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C1")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))))) & (Bool (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C1")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))))) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C1")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2")))))  ")" )  ")" ))); 
 







theorem :: CAT_5:5 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r2_subset_1 :::"meets"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))))) "holds"  (Bool (Set (Set (Var "C1"))  ($#k3_cat_5 :::"/\"::: )  (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C2"))  ($#k3_cat_5 :::"/\"::: )  (Set (Var "C1")))))) ; 
 
theorem :: CAT_5:6 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r2_subset_1 :::"meets"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "C1"))  ($#k3_cat_5 :::"/\"::: )  (Set (Var "C2"))) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C1"))) & (Bool (Set (Set (Var "C1"))  ($#k3_cat_5 :::"/\"::: )  (Set (Var "C2"))) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "C2")))  ")" ))) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); func  :::"Image"::: "F" ->   ($#v1_cat_1 :::"strict"::: )     ($#m3_cat_2 :::"Subcategory"::: )   "of" "D" means :: CAT_5:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k7_cat_1 :::"Obj"::: )  "F" ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  "F")  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)) & (Bool  "("   "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" "D"  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k7_cat_1 :::"Obj"::: )  "F" ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  "F")  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "E"))))) "holds"  (Bool it "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "E")))  ")" )  ")" ); end; 







:: deftheorem    defines :::"Image"::: CAT_5:def 3 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "F")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "F")) ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b4")))) & (Bool  "("   "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "F")) ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "E"))))) "holds"  (Bool (Set (Var "b4")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "E")))  ")" )  ")" )  ")" )))); 
 
theorem :: CAT_5:7 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "E"))))) "holds"  (Bool (Set (Var "F")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E")))))) ; 
 
theorem :: CAT_5:8 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D")) "holds"  (Bool (Set (Var "F")) "is"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "F")))))) ; 
 
theorem :: CAT_5:9 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D"))  "st" (Bool (Bool (Set (Var "F"))  ($#r1_funct_2 :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "G")))))))) ; 
 begin  definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"categorial":::  means :: CAT_5:def 4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Var "x")) "is"   ($#l1_cat_1 :::"Category":::))); end; 




:: deftheorem    defines :::"categorial"::: CAT_5:def 4 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_cat_5 :::"categorial"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) "holds"  (Bool (Set (Var "x")) "is"   ($#l1_cat_1 :::"Category":::)))  ")" )); 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; redefine attr "X" is  :::"categorial":::  means :: CAT_5:def 5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "X" "holds"  (Bool (Set (Var "x")) "is"   ($#l1_cat_1 :::"Category":::))); end; 




:: deftheorem    defines :::"categorial"::: CAT_5:def 5 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_cat_5 :::"categorial"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Var "x")) "is"   ($#l1_cat_1 :::"Category":::)))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_cat_5 :::"categorial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_cat_5 :::"categorial"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "X" ->   ($#l1_cat_1 :::"Category":::); end; definitionlet "C" be   ($#l1_cat_1 :::"Category":::); attr "C" is  :::"Categorial":::  means :: CAT_5:def 6 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C") "is"   ($#v2_cat_5 :::"categorial"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" "C"  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k10_cat_1 :::"id"::: )  (Set (Var "A")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "m")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "m"))))) "holds"  (Bool  "ex" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ))))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "G")) ($#k4_tarski :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set  "(" (Set (Var "G"))  ($#k9_cat_1 :::"*"::: )  (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) )))))  ")" )  ")" ); end; 




:: deftheorem    defines :::"Categorial"::: CAT_5:def 6 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v3_cat_5 :::"Categorial"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "is"   ($#v2_cat_5 :::"categorial"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k10_cat_1 :::"id"::: )  (Set (Var "A")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "m")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "m"))))) "holds"  (Bool  "ex" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ))))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "G")) ($#k4_tarski :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set  "(" (Set (Var "G"))  ($#k9_cat_1 :::"*"::: )  (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) )))))  ")" )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v2_cat_1 :::"Category-like"::: )     ($#v3_cat_1 :::"transitive"::: )     ($#v4_cat_1 :::"associative"::: )     ($#v5_cat_1 :::"reflexive"::: )     ($#v6_cat_1 :::"with_identities"::: )     ($#v3_cat_5 :::"Categorial"::: )    ->   ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    for    ($#l1_cat_1 :::"CatStr"::: )  ; 
end; 
theorem :: CAT_5:10 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "D"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "D"))) "#)" )) & (Bool (Set (Var "C")) "is"   ($#v3_cat_5 :::"Categorial"::: )  )) "holds"  (Bool (Set (Var "D")) "is"   ($#v3_cat_5 :::"Categorial"::: )  )) ; 
 
theorem :: CAT_5:11 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set   ($#k3_cat_1 :::"1Cat"::: )   "(" (Set (Var "C")) "," (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "C")) "," (Set (Var "C")) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k10_cat_1 :::"id"::: )  (Set (Var "C")) ")" ) ($#k4_tarski :::"]"::: ) ) ")" ) "is"   ($#v3_cat_5 :::"Categorial"::: )  )) ; 
 registration
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"::: )     ($#v3_cat_5 :::"Categorial"::: )    for    ($#l1_cat_1 :::"CatStr"::: )  ; 
end; 
theorem :: CAT_5:12 (Bool  "for" (Set (Var "C")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Var "a")) "is"   ($#l1_cat_1 :::"Category":::)))) ; 
 
theorem :: CAT_5:13 (Bool  "for" (Set (Var "C")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_cat_5 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_cat_5 :::"`12"::: )  ))  ")" ))) ; 
 definitionlet "C" be   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::); let "m" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); :: original: :::"`11"::: redefine func "m" :::"`11":::  ->   ($#l1_cat_1 :::"Category":::); :: original: :::"`12"::: redefine func "m" :::"`12":::  ->   ($#l1_cat_1 :::"Category":::); end; 
theorem :: CAT_5:14 (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))))) "holds"  (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C2"))) "#)" ))) ; 
 registrationlet "C" be   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::); 
cluster   ->   ($#v3_cat_5 :::"Categorial"::: )    for    ($#m3_cat_2 :::"Subcategory"::: )   "of" "C"; 
end; 
theorem :: CAT_5:15 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "D"))))) "holds"  (Bool (Set (Var "C")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D")))) ; 
 definitionlet "a" be    ($#m1_hidden :::"set"::: )  ; assume 
(Bool (Set (Const "a")) "is"   ($#l1_cat_1 :::"Category":::))
 ; func  :::"cat"::: "a" ->   ($#l1_cat_1 :::"Category":::) equals :: CAT_5:def 7 "a"; end; 






:: deftheorem    defines :::"cat"::: CAT_5:def 7 :  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a")) "is"   ($#l1_cat_1 :::"Category":::))) "holds"  (Bool (Set   ($#k7_cat_5 :::"cat"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))); 
 
theorem :: CAT_5:16 (Bool  "for" (Set (Var "C")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k7_cat_5 :::"cat"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 definitionlet "C" be   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::); let "m" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); :: original: :::"`2"::: redefine func "m" :::"`2":::  ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set   ($#k7_cat_5 :::"cat"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  "m" ")" )) "," (Set   ($#k7_cat_5 :::"cat"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  "m" ")" )); end; 
theorem :: CAT_5:17 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_cat_5 :::"categorial"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"    ($#m1_cat_5 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "G"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k9_cat_1 :::"*"::: )  (Set (Var "F")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_cat_5 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k10_cat_1 :::"id"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_cat_5 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "F")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))) "iff" (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))  ")" )  ")" )))) ; 
 
theorem :: CAT_5:18 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_cat_5 :::"categorial"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_cat_5 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "F")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C1"))) "iff" (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))  ")" ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_cat_5 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "F")) ($#k1_domain_1 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C2"))) "iff" (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "C1"))  ($#r1_hidden :::"="::: )  (Set (Var "C2")))))) ; 
 definitionlet "IT" be   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::); attr "IT" is  :::"full":::  means :: CAT_5:def 8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Object":::) "of" "IT") & (Bool (Set (Var "b")) "is"   ($#m1_subset_1 :::"Object":::) "of" "IT")) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "a")) "," (Set (Var "b")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" "IT"))); end; 




:: deftheorem    defines :::"full"::: CAT_5:def 8 :  (Bool  "for" (Set (Var "IT")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_cat_5 :::"full"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "IT"))) & (Bool (Set (Var "b")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "IT")))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "a")) "," (Set (Var "b")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "IT")))))  ")" )); 
 registration
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"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )     ($#v3_cat_5 :::"Categorial"::: )     ($#v4_cat_5 :::"full"::: )    for    ($#l1_cat_1 :::"CatStr"::: )  ; 
end; 
theorem :: CAT_5:19 (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#v3_cat_5 :::"Categorial"::: )     ($#v4_cat_5 :::"full"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))))) "holds"  (Bool (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C1"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C2"))) "," (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "C2"))) "#)" ))) ; 
 
theorem :: CAT_5:20 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_cat_5 :::"categorial"::: )     ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "C")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v3_cat_5 :::"Categorial"::: )     ($#v4_cat_5 :::"full"::: )    ($#l1_cat_1 :::"Category":::) "st" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: CAT_5:21 (Bool  "for" (Set (Var "C")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "D")) "being"   ($#v3_cat_5 :::"Categorial"::: )     ($#v4_cat_5 :::"full"::: )    ($#l1_cat_1 :::"Category":::)  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "D"))))) "holds"  (Bool (Set (Var "C")) "is"    ($#m3_cat_2 :::"Subcategory"::: )   "of" (Set (Var "D"))))) ; 
 
theorem :: CAT_5:22 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "D1")) "," (Set (Var "D2")) "being"   ($#v3_cat_5 :::"Categorial"::: )    ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F1")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D1"))  (Bool  "for" (Set (Var "F2")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D2"))  "st" (Bool (Bool (Set (Var "F1"))  ($#r1_funct_2 :::"="::: )  (Set (Var "F2")))) "holds"  (Bool (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_cat_5 :::"Image"::: )  (Set (Var "F2")))))))) ; 
 begin  definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "o" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func  :::"Hom"::: "o" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") equals :: CAT_5:def 9 (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "C")  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) "o" ($#k6_domain_1 :::"}"::: ) )); func "o" :::"Hom":::  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") equals :: CAT_5:def 10 (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "C")  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) "o" ($#k6_domain_1 :::"}"::: ) )); end; 












:: deftheorem    defines :::"Hom"::: CAT_5:def 9 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "C")))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ))))); 
 
:: deftheorem    defines :::"Hom"::: CAT_5:def 10 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "C")))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ))))); 
 registrationlet "C" be   ($#l1_cat_1 :::"Category":::); let "o" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); 
cluster (Set   ($#k9_cat_5 :::"Hom"::: )  "o") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set "o"  ($#k10_cat_5 :::"Hom"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: CAT_5:23 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "a")))) "iff" (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 
theorem :: CAT_5:24 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k10_cat_5 :::"Hom"::: )  )) "iff" (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 
theorem :: CAT_5:25 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_cat_5 :::"Hom"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k9_cat_5 :::"Hom"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: CAT_5:26 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k10_cat_5 :::"Hom"::: )  )) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_cat_5 :::"Hom"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )))  ")" ))) ; 
 
theorem :: CAT_5:27 (Bool  "for" (Set (Var "C")) "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"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "g")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_cat_5 :::"Hom"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: CAT_5:28 (Bool  "for" (Set (Var "C")) "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"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )  ($#k10_cat_5 :::"Hom"::: )  ) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k10_cat_5 :::"Hom"::: )  ))))) ; 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "o" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "C" :::"-SliceCat"::: "o" ->   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::) means :: CAT_5:def 11 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_cat_5 :::"Hom"::: )  "o")) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  "o")  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f"))))) "holds"  (Bool (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" it))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" it (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  "o")(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C" "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f"))))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" it  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  "o")  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f1")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f2")) ($#k10_cat_2 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "f2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f1")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))  ")" )  ")" ); func "o" :::"-SliceCat"::: "C" ->   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::) means :: CAT_5:def 12 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set "o"  ($#k10_cat_5 :::"Hom"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set "o"  ($#k10_cat_5 :::"Hom"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" it))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" it (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set "o"  ($#k10_cat_5 :::"Hom"::: )  )(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C" "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" it  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set "o"  ($#k10_cat_5 :::"Hom"::: )  )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "C"  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f1")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f2")) ($#k10_cat_2 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "f2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f1")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))  ")" )  ")" ); end; 












:: deftheorem    defines :::"-SliceCat"::: CAT_5:def 11 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set (Var "o")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f"))))) "holds"  (Bool (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3"))))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f"))))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3"))  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f1")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f2")) ($#k10_cat_2 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "f2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f1")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))  ")" )  ")" )  ")" )))); 
 
:: deftheorem    defines :::"-SliceCat"::: CAT_5:def 12 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_cat_1 :::"strict"::: )     ($#v1_cat_5 :::"with_triple-like_morphisms"::: )    ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3"))))  ")" ) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3"))  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f1")) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set (Var "m2"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set (Var "f2")) ($#k10_cat_2 :::"]"::: ) ))) "holds"  (Bool (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "a3")) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "f2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f1")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))  ")" )  ")" )  ")" )))); 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "o" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "m" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set (Const "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set (Const "o")) ")" ); :: original: :::"`2"::: redefine func "m" :::"`2":::  ->   ($#m1_subset_1 :::"Morphism":::) "of" "C"; :: original: :::"`11"::: redefine func "m" :::"`11":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  "o"); :: original: :::"`12"::: redefine func "m" :::"`12":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  "o"); end; 
theorem :: CAT_5:29 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set (Var "a")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set (Var "m"))  ($#k14_cat_5 :::"`11"::: )  ")" ) "," (Set  "(" (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k13_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  "(" (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set  "(" (Set (Var "m"))  ($#k13_cat_5 :::"`2"::: )  ")" ))) & (Bool (Set (Set (Var "m"))  ($#k14_cat_5 :::"`11"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k13_cat_5 :::"`2"::: )  ")" ))) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k14_cat_5 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ))  ")" )))) ; 
 
theorem :: CAT_5:30 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k9_cat_5 :::"Hom"::: )  (Set (Var "o")))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  "(" (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set (Var "o")) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k9_cat_2 :::"]"::: ) ) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "o" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "m" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set (Const "o"))  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Const "C")) ")" ); :: original: :::"`2"::: redefine func "m" :::"`2":::  ->   ($#m1_subset_1 :::"Morphism":::) "of" "C"; :: original: :::"`11"::: redefine func "m" :::"`11":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "o"  ($#k10_cat_5 :::"Hom"::: )  ); :: original: :::"`12"::: redefine func "m" :::"`12":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set "o"  ($#k10_cat_5 :::"Hom"::: )  ); end; 
theorem :: CAT_5:31 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set (Var "a"))  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  ")" ) "," (Set  "(" (Set (Var "m"))  ($#k18_cat_5 :::"`12"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k16_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  "(" (Set (Var "m"))  ($#k16_cat_5 :::"`2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set  "(" (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "m"))  ($#k16_cat_5 :::"`2"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k18_cat_5 :::"`12"::: )  )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k18_cat_5 :::"`12"::: )  ))  ")" )))) ; 
 
theorem :: CAT_5:32 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "f")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Set (Var "o"))  ($#k10_cat_5 :::"Hom"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  "(" (Set (Var "o"))  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C")) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k9_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k9_cat_2 :::"]"::: ) ) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; 
 begin  definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "f" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func  :::"SliceFunctor"::: "f" ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set "C"  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  "f" ")" )) "," (Set "C"  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  "f" ")" )) means :: CAT_5:def 13 (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" "C"  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  "f" ")" ) ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" "f"  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k14_cat_5 :::"`11"::: )  ")" ) ")" ) "," (Set  "(" "f"  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ")" ) ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k13_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) ))); func  :::"SliceContraFunctor"::: "f" ->    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Set  "("  ($#k4_graph_1 :::"cod"::: )  "f" ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  "C") "," (Set (Set  "("  ($#k3_graph_1 :::"dom"::: )  "f" ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  "C") means :: CAT_5:def 14 (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set  "("  ($#k4_graph_1 :::"cod"::: )  "f" ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  "C" ")" ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  "f" ")" ) "," (Set  "(" (Set  "(" (Set (Var "m"))  ($#k18_cat_5 :::"`12"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  "f" ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k16_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) ))); end; 












:: deftheorem    defines :::"SliceFunctor"::: CAT_5:def 13 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" )) "," (Set (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k19_cat_5 :::"SliceFunctor"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set (Var "C"))  ($#k11_cat_5 :::"-SliceCat"::: )  (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k14_cat_5 :::"`11"::: )  ")" ) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "m"))  ($#k15_cat_5 :::"`12"::: )  ")" ) ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k13_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) )))  ")" )))); 
 
:: deftheorem    defines :::"SliceContraFunctor"::: CAT_5:def 14 :  (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C"))) "," (Set (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_cat_5 :::"SliceContraFunctor"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "(" (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" )  ($#k12_cat_5 :::"-SliceCat"::: )  (Set (Var "C")) ")" ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_cat_2 :::"["::: ) (Set  ($#k10_cat_2 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "m"))  ($#k17_cat_5 :::"`11"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "m"))  ($#k18_cat_5 :::"`12"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "m"))  ($#k16_cat_5 :::"`2"::: )  ")" ) ($#k10_cat_2 :::"]"::: ) )))  ")" )))); 
 
theorem :: CAT_5:33 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k19_cat_5 :::"SliceFunctor"::: )  (Set  "(" (Set (Var "g"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_cat_5 :::"SliceFunctor"::: )  (Set (Var "g")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k19_cat_5 :::"SliceFunctor"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: CAT_5:34 (Bool  "for" (Set (Var "C")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k20_cat_5 :::"SliceContraFunctor"::: )  (Set  "(" (Set (Var "g"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_cat_5 :::"SliceContraFunctor"::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k20_cat_5 :::"SliceContraFunctor"::: )  (Set (Var "g")) ")" ))))) ;