:: FUNCTOR1  semantic presentation begin  






registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )    for    ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
end; registrationlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  ; 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )    for    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" "A"; 
end; registrationlet "C1", "C2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )  ; let "F" be   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Const "C1")) "," (Set (Const "C2")); let "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Const "C1")); 
cluster (Set "F"  ($#k14_functor0 :::"|"::: )  "A") ->   ($#v8_functor0 :::"feasible"::: )   ; 
end; begin  registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_relat_1 :::"id"::: )  "X") ->   ($#v2_funct_2 :::"onto"::: )   ; 
end; 
theorem :: FUNCTOR1:1 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Var "D")))) "holds"  (Bool (Set   ($#k6_funct_3 :::"incl"::: )  (Set (Var "C")))  ($#r1_funct_2 :::"="::: )  (Set (Set  "("  ($#k6_funct_3 :::"incl"::: )  (Set (Var "B")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_funct_3 :::"incl"::: )  (Set (Var "D")) ")" )))))) ; 
 
theorem :: FUNCTOR1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X"))))) ; 
 
theorem :: FUNCTOR1:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v3_funct_2 :::"bijective"::: )  )) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))) & (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )  ")" )))))) ; 
 begin  
theorem :: FUNCTOR1:4 (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "D")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Var "D")))) "holds"  (Bool (Set   ($#k10_functor0 :::"incl"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_functor0 :::"incl"::: )  (Set (Var "B")) ")" )  ($#k13_functor0 :::"*"::: )  (Set  "("  ($#k10_functor0 :::"incl"::: )  (Set (Var "D")) ")" ))))))) ; 
 
theorem :: FUNCTOR1:5 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  )) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F"))) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F"))) "is"   ($#v1_msualg_3 :::""1-1""::: )  )  ")" ))) ; 
 
theorem :: FUNCTOR1:6 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v4_functor0 :::"one-to-one"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v4_functor0 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v4_functor0 :::"one-to-one"::: )  ))))) ; 
 
theorem :: FUNCTOR1:7 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v17_functor0 :::"faithful"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v17_functor0 :::"faithful"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v17_functor0 :::"faithful"::: )  ))))) ; 
 
theorem :: FUNCTOR1:8 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v5_functor0 :::"onto"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v5_functor0 :::"onto"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v5_functor0 :::"onto"::: )  ))))) ; 
 
theorem :: FUNCTOR1:9 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v18_functor0 :::"full"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v18_functor0 :::"full"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v18_functor0 :::"full"::: )  ))))) ; 
 
theorem :: FUNCTOR1:10 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v19_functor0 :::"injective"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v19_functor0 :::"injective"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v19_functor0 :::"injective"::: )  ))))) ; 
 
theorem :: FUNCTOR1:11 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v20_functor0 :::"surjective"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v20_functor0 :::"surjective"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v20_functor0 :::"surjective"::: )  ))))) ; 
 
theorem :: FUNCTOR1:12 (Bool  "for" (Set (Var "C1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "C2")) "," (Set (Var "C3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l1_altcat_1 :::"AltGraph"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2"))  (Bool  "for" (Set (Var "G")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C2")) "," (Set (Var "C3"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v21_functor0 :::"bijective"::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k13_functor0 :::"*"::: )  (Set (Var "F"))) "is"   ($#v21_functor0 :::"bijective"::: )  ))))) ; 
 begin  
theorem :: FUNCTOR1:13 (Bool  "for" (Set (Var "A")) "," (Set (Var "I")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_altcat_2 :::"reflexive"::: )     ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "D")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Var "D")))) "holds"  (Bool  "for" (Set (Var "F")) "being"    ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "I")) "holds"  (Bool (Set (Set (Var "F"))  ($#k14_functor0 :::"|"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k14_functor0 :::"|"::: )  (Set (Var "B")) ")" )  ($#k14_functor0 :::"|"::: )  (Set (Var "D"))))))))) ; 
 
theorem :: FUNCTOR1:14 (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_altcat_2 :::"SubCatStr"::: )   "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v2_altcat_2 :::"full"::: )  ) "iff" (Bool (Set   ($#k10_functor0 :::"incl"::: )  (Set (Var "B"))) "is"   ($#v18_functor0 :::"full"::: )  )  ")" ))) ; 
 begin  
theorem :: FUNCTOR1:15 (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v10_functor0 :::"Covariant"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v18_functor0 :::"full"::: )  ) "iff" (Bool  "for" (Set (Var "o1")) "," (Set (Var "o2")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds"  (Bool (Set   ($#k5_functor0 :::"Morph-Map"::: )   "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ) "is"   ($#v2_funct_2 :::"onto"::: )  ))  ")" ))) ; 
 
theorem :: FUNCTOR1:16 (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v10_functor0 :::"Covariant"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v17_functor0 :::"faithful"::: )  ) "iff" (Bool  "for" (Set (Var "o1")) "," (Set (Var "o2")) "being"   ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds"  (Bool (Set   ($#k5_functor0 :::"Morph-Map"::: )   "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))  ")" ))) ; 
 begin  
theorem :: FUNCTOR1:17 (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )   "holds"  (Bool (Set (Set  "("  ($#k12_functor0 :::"id"::: )  (Set (Var "A")) ")" )  ($#k15_functor0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A"))))) ; 
 
theorem :: FUNCTOR1:18 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  )) "holds"  (Bool  "for" (Set (Var "G")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "B")) "," (Set (Var "A"))  "st" (Bool (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "G"))) "#)" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k15_functor0 :::"""::: )  ))) "holds"  (Bool (Set (Set (Var "F"))  ($#k13_functor0 :::"*"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "B"))))))) ; 
 
theorem :: FUNCTOR1:19 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k15_functor0 :::"""::: )  ")" )  ($#k13_functor0 :::"*"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_functor0 :::"id"::: )  (Set (Var "A")))))) ; 
 
theorem :: FUNCTOR1:20 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k15_functor0 :::"""::: )  ")" )  ($#k15_functor0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "F"))) "#)" )))) ; 
 
theorem :: FUNCTOR1:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_altcat_1 :::"transitive"::: )     ($#v12_altcat_1 :::"with_units"::: )     ($#v1_altcat_2 :::"reflexive"::: )     ($#l2_altcat_1 :::"AltCatStr"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "F")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "B")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "GI")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "B")) "," (Set (Var "A"))  (Bool  "for" (Set (Var "FI")) "being"   ($#v8_functor0 :::"feasible"::: )     ($#l2_functor0 :::"FunctorStr"::: )   "over" (Set (Var "C")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v21_functor0 :::"bijective"::: )  ) & (Bool (Set (Var "G")) "is"   ($#v21_functor0 :::"bijective"::: )  ) & (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "GI"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "GI"))) "#)" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k15_functor0 :::"""::: )  )) & (Bool (Set   ($#g2_functor0 :::"FunctorStr"::: )  "(#"  (Set  "the"  ($#u1_functor0 :::"ObjectMap"::: )  "of" (Set (Var "FI"))) "," (Set  "the"  ($#u2_functor0 :::"MorphMap"::: )  "of" (Set (Var "FI"))) "#)" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k15_functor0 :::"""::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k13_functor0 :::"*"::: )  (Set (Var "G")) ")" )  ($#k15_functor0 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "GI"))  ($#k13_functor0 :::"*"::: )  (Set (Var "FI"))))))))) ;