:: RINGCAT1  semantic presentation begin  









definitionlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "IT" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G")) "," (Set (Const "H")); attr "IT" is  :::"linear":::  means :: RINGCAT1:def 1 (Bool  "("  (Bool "IT" "is"   ($#v13_vectsp_1 :::"additive"::: )  ) & (Bool "IT" "is"   ($#v1_group_6 :::"multiplicative"::: )  ) & (Bool "IT" "is"   ($#v6_group_1 :::"unity-preserving"::: )  )  ")" ); end; 






:: deftheorem    defines :::"linear"::: RINGCAT1:def 1 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_ringcat1 :::"linear"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v13_vectsp_1 :::"additive"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v1_group_6 :::"multiplicative"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v6_group_1 :::"unity-preserving"::: )  )  ")" )  ")" ))); 
 registrationlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; 
cluster bbbadV1_FUNCT_1() bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H"))   ($#v1_ringcat1 :::"linear"::: )    ->   ($#v6_group_1 :::"unity-preserving"::: )     ($#v1_group_6 :::"multiplicative"::: )     ($#v13_vectsp_1 :::"additive"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); 

cluster bbbadV1_FUNCT_1() bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H"))   ($#v6_group_1 :::"unity-preserving"::: )     ($#v1_group_6 :::"multiplicative"::: )     ($#v13_vectsp_1 :::"additive"::: )    ->   ($#v1_ringcat1 :::"linear"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: RINGCAT1:1 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_ringcat1 :::"linear"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v1_ringcat1 :::"linear"::: )  )) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v1_ringcat1 :::"linear"::: )  )))) ; 
 definitionattr "c1" is  :::"strict"::: ; struct  :::"RingMorphismStr":::  -> ; aggr :::"RingMorphismStr":::(# :::"Dom":::, :::"Cod":::, :::"Fun"::: #) ->    ($#l1_ringcat1 :::"RingMorphismStr"::: )  ; sel  :::"Dom"::: "c1" ->   ($#l6_algstr_0 :::"Ring":::); sel  :::"Cod"::: "c1" ->   ($#l6_algstr_0 :::"Ring":::); sel  :::"Fun"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" "c1") "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" "c1"); end; 


definitionlet "f" be    ($#l1_ringcat1 :::"RingMorphismStr"::: )  ; func  :::"dom"::: "f" ->   ($#l6_algstr_0 :::"Ring":::) equals :: RINGCAT1:def 2 (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" "f"); func  :::"cod"::: "f" ->   ($#l6_algstr_0 :::"Ring":::) equals :: RINGCAT1:def 3 (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" "f"); func  :::"fun"::: "f" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" "f") "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" "f") equals :: RINGCAT1:def 4 (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" "f"); end; 















:: deftheorem    defines :::"dom"::: RINGCAT1:def 2 :  (Bool  "for" (Set (Var "f")) "being"    ($#l1_ringcat1 :::"RingMorphismStr"::: )   "holds"  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" (Set (Var "f"))))); 
 
:: deftheorem    defines :::"cod"::: RINGCAT1:def 3 :  (Bool  "for" (Set (Var "f")) "being"    ($#l1_ringcat1 :::"RingMorphismStr"::: )   "holds"  (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" (Set (Var "f"))))); 
 
:: deftheorem    defines :::"fun"::: RINGCAT1:def 4 :  (Bool  "for" (Set (Var "f")) "being"    ($#l1_ringcat1 :::"RingMorphismStr"::: )   "holds"  (Bool (Set   ($#k3_ringcat1 :::"fun"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" (Set (Var "f"))))); 
 







registrationlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; 
cluster (Set   ($#k3_struct_0 :::"id"::: )  "G") ->   ($#v1_ringcat1 :::"linear"::: )   ; 
end; definitionlet "IT" be    ($#l1_ringcat1 :::"RingMorphismStr"::: )  ; attr "IT" is  :::"RingMorphism-like":::  means :: RINGCAT1:def 5 (Bool (Set   ($#k3_ringcat1 :::"fun"::: )  "IT") "is"   ($#v1_ringcat1 :::"linear"::: )  ); end; 




:: deftheorem    defines :::"RingMorphism-like"::: RINGCAT1:def 5 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_ringcat1 :::"RingMorphismStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_ringcat1 :::"RingMorphism-like"::: )  ) "iff" (Bool (Set   ($#k3_ringcat1 :::"fun"::: )  (Set (Var "IT"))) "is"   ($#v1_ringcat1 :::"linear"::: )  )  ")" )); 
 registration
cluster   ($#v2_ringcat1 :::"strict"::: )     ($#v3_ringcat1 :::"RingMorphism-like"::: )    for    ($#l1_ringcat1 :::"RingMorphismStr"::: )  ; 
end; definitionmode RingMorphism is   ($#v3_ringcat1 :::"RingMorphism-like"::: )     ($#l1_ringcat1 :::"RingMorphismStr"::: )  ; end; definitionlet "G" be   ($#l6_algstr_0 :::"Ring":::); func  :::"ID"::: "G" ->   ($#l1_ringcat1 :::"RingMorphism":::) equals :: RINGCAT1:def 6 (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  "G" "," "G" "," (Set  "("  ($#k3_struct_0 :::"id"::: )  "G" ")" ) "#)" ); end; 





:: deftheorem    defines :::"ID"::: RINGCAT1:def 6 :  (Bool  "for" (Set (Var "G")) "being"   ($#l6_algstr_0 :::"Ring":::) "holds"  (Bool (Set   ($#k4_ringcat1 :::"ID"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G")) "," (Set (Var "G")) "," (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "G")) ")" ) "#)" ))); 
 registrationlet "G" be   ($#l6_algstr_0 :::"Ring":::); 
cluster (Set   ($#k4_ringcat1 :::"ID"::: )  "G") ->   ($#v2_ringcat1 :::"strict"::: )   ; 
end; 


definitionlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); pred "G" :::"<="::: "H" means :: RINGCAT1:def 7 (Bool  "ex" (Set (Var "F")) "being"   ($#l1_ringcat1 :::"RingMorphism":::) "st"  (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  "G") & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  "H")  ")" )); reflexivity  
(Bool  "for" (Set (Var "G")) "being"   ($#l6_algstr_0 :::"Ring":::) (Bool  "ex" (Set (Var "F")) "being"   ($#l1_ringcat1 :::"RingMorphism":::) "st"  (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "G")))  ")" )))
 ; end; 





:: deftheorem    defines :::"<="::: RINGCAT1:def 7 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::) "holds"   (Bool  "("  (Bool (Set (Var "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "H"))) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#l1_ringcat1 :::"RingMorphism":::) "st"  (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "H")))  ")" ))  ")" )); 
 definitionlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); assume 
(Bool (Set (Const "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Const "H")))
 ; mode  :::"Morphism":::  "of" "G" "," "H" ->   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) means :: RINGCAT1:def 8 (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "G") & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  it)  ($#r1_hidden :::"="::: )  "H")  ")" ); end; 







:: deftheorem    defines :::"Morphism"::: RINGCAT1:def 8 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "H")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "H")))  ")" )  ")" ))); 
 registrationlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); 
cluster   ($#v2_ringcat1 :::"strict"::: )     ($#v3_ringcat1 :::"RingMorphism-like"::: )    for    ($#m1_ringcat1 :::"Morphism"::: )   "of" "G" "," "H"; 
end; definitionlet "G" be   ($#l6_algstr_0 :::"Ring":::); :: original: :::"ID"::: redefine func  :::"ID"::: "G" ->   ($#v2_ringcat1 :::"strict"::: )     ($#m1_ringcat1 :::"Morphism"::: )   "of" "G" "," "G"; end; 
theorem :: RINGCAT1:2 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::) "st"  (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3"))) & (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" (Set (Var "g"))) "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" (Set (Var "g"))) "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" (Set (Var "g"))) "#)" ) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" (Set (Var "f"))) "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" (Set (Var "f"))) "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" (Set (Var "f"))) "#)" ) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G2")))  ")" ))) ; 
 
theorem :: RINGCAT1:3 (Bool  "for" (Set (Var "F")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "F"))) "," (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F")))) & (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "F")))  ($#r1_ringcat1 :::"<="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F"))))  ")" )) ; 
 
theorem :: RINGCAT1:4 (Bool  "for" (Set (Var "F")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) (Bool  "ex" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::)(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )) & (Bool (Set (Var "f")) "is"   ($#v1_ringcat1 :::"linear"::: )  )  ")" )))) ; 
 definitionlet "G", "F" be   ($#l1_ringcat1 :::"RingMorphism":::); assume 
(Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Const "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Const "F"))))
 ; func "G" :::"*"::: "F" ->   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) means :: RINGCAT1:def 9 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2"))  "st" (Bool (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" "G") "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" "G") "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" "G") "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" "F") "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" "F") "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" "F") "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G3")) "," (Set  "(" (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) "#)" ))))); end; 







:: deftheorem    defines :::"*"::: RINGCAT1:def 9 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "F")) "being"   ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2"))  "st" (Bool (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" (Set (Var "G"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set  "the"  ($#u1_ringcat1 :::"Dom"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u2_ringcat1 :::"Cod"::: )  "of" (Set (Var "F"))) "," (Set  "the"  ($#u3_ringcat1 :::"Fun"::: )  "of" (Set (Var "F"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G3")) "," (Set  "(" (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")) ")" ) "#)" )))))  ")" ))); 
 
theorem :: RINGCAT1:5 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::)  "st" (Bool (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3")))) "holds"  (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3")))) ; 
 
theorem :: RINGCAT1:6 (Bool  "for" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G1")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "G")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G2")) "," (Set (Var "G3"))  (Bool  "for" (Set (Var "F")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G2"))  "st" (Bool (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "F"))) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G3")))))) ; 
 definitionlet "G1", "G2", "G3" be   ($#l6_algstr_0 :::"Ring":::); let "G" be    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Const "G2")) "," (Set (Const "G3")); let "F" be    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Const "G1")) "," (Set (Const "G2")); assume 
(Bool  "("  (Bool (Set (Const "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Const "G2"))) & (Bool (Set (Const "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Const "G3")))  ")" )
 ; func "G" :::"*'"::: "F" ->   ($#v2_ringcat1 :::"strict"::: )     ($#m1_ringcat1 :::"Morphism"::: )   "of" "G1" "," "G3" equals :: RINGCAT1:def 10 (Set "G"  ($#k6_ringcat1 :::"*"::: )  "F"); end; 










:: deftheorem    defines :::"*'"::: RINGCAT1:def 10 :  (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "G")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G2")) "," (Set (Var "G3"))  (Bool  "for" (Set (Var "F")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G2"))  "st" (Bool (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_ringcat1 :::"*'"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "F"))))))); 
 
theorem :: RINGCAT1:7 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"   ($#l6_algstr_0 :::"Ring":::)(Bool  "ex" (Set (Var "f0")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2"))(Bool  "ex" (Set (Var "g0")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "G3")) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f0")) "#)" )) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g0")) "#)" )) & (Bool (Set (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_ringcat1 :::"RingMorphismStr"::: )  "(#"  (Set (Var "G1")) "," (Set (Var "G3")) "," (Set  "(" (Set (Var "g0"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f0")) ")" ) "#)" ))  ")" ))))) ; 
 
theorem :: RINGCAT1:8 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set  "(" (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "g"))))  ")" )) ; 
 
theorem :: RINGCAT1:9 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G4")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G2"))  (Bool  "for" (Set (Var "g")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G2")) "," (Set (Var "G3"))  (Bool  "for" (Set (Var "h")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G3")) "," (Set (Var "G4"))  "st" (Bool (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3"))) & (Bool (Set (Var "G3"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G4")))) "holds"  (Bool (Set (Set (Var "h"))  ($#k6_ringcat1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "h"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "g")) ")" )  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")))))))) ; 
 
theorem :: RINGCAT1:10 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "g")))) & (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k6_ringcat1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "h"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "g")) ")" )  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f"))))) ; 
 
theorem :: RINGCAT1:11 (Bool  "for" (Set (Var "G")) "being"   ($#l6_algstr_0 :::"Ring":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set  "("  ($#k5_ringcat1 :::"ID"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set  "("  ($#k5_ringcat1 :::"ID"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k2_ringcat1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set  "("  ($#k5_ringcat1 :::"ID"::: )  (Set (Var "G")) ")" )  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))  ")" ) & (Bool  "("   "for" (Set (Var "g")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)  "st" (Bool (Bool (Set   ($#k1_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set  "("  ($#k5_ringcat1 :::"ID"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")" )  ")" )) ; 
 definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"Ring_DOMAIN-like":::  means :: RINGCAT1:def 11 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "IT" "holds"  (Bool (Set (Var "x")) "is"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Ring":::))); end; 




:: deftheorem    defines :::"Ring_DOMAIN-like"::: RINGCAT1:def 11 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_ringcat1 :::"Ring_DOMAIN-like"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "IT")) "holds"  (Bool (Set (Var "x")) "is"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Ring":::)))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_ringcat1 :::"Ring_DOMAIN-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Ring_DOMAIN is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_ringcat1 :::"Ring_DOMAIN-like"::: )     ($#m1_hidden :::"set"::: )  ; end; 


definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "V" ->   ($#l6_algstr_0 :::"Ring":::); end; registrationlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v36_algstr_0 :::"strict"::: )   bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1()   ($#v1_group_1 :::"unital"::: )     ($#v3_group_1 :::"associative"::: )     ($#v1_vectsp_1 :::"right-distributive"::: )     ($#v2_vectsp_1 :::"left-distributive"::: )     ($#v3_vectsp_1 :::"right_unital"::: )     ($#v4_vectsp_1 :::"well-unital"::: )   bbbadV5_VECTSP_1()   ($#v6_vectsp_1 :::"left_unital"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "V"; 
end; definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"RingMorphism_DOMAIN-like":::  means :: RINGCAT1:def 12 (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"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::))); end; 




:: deftheorem    defines :::"RingMorphism_DOMAIN-like"::: RINGCAT1:def 12 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_ringcat1 :::"RingMorphism_DOMAIN-like"::: )  ) "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"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::)))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_ringcat1 :::"RingMorphism_DOMAIN-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode RingMorphism_DOMAIN is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_ringcat1 :::"RingMorphism_DOMAIN-like"::: )     ($#m1_hidden :::"set"::: )  ; end; definitionlet "M" be   ($#m1_hidden :::"RingMorphism_DOMAIN":::); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "M" ->   ($#l1_ringcat1 :::"RingMorphism":::); end; registrationlet "M" be   ($#m1_hidden :::"RingMorphism_DOMAIN":::); 
cluster   ($#v2_ringcat1 :::"strict"::: )     ($#v3_ringcat1 :::"RingMorphism-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "M"; 
end; 
theorem :: RINGCAT1:12 (Bool  "for" (Set (Var "f")) "being"   ($#v2_ringcat1 :::"strict"::: )    ($#l1_ringcat1 :::"RingMorphism":::) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is"   ($#m1_hidden :::"RingMorphism_DOMAIN":::))) ; 
 definitionlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); mode  :::"RingMorphism_DOMAIN":::  "of" "G" "," "H" ->   ($#m1_hidden :::"RingMorphism_DOMAIN":::) means :: RINGCAT1:def 13 (Bool  "for" (Set (Var "x")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" it "holds"  (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" "G" "," "H")); end; 






:: deftheorem    defines :::"RingMorphism_DOMAIN"::: RINGCAT1:def 13 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"RingMorphism_DOMAIN":::) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set (Var "b3")) "holds"  (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))))  ")" ))); 
 
theorem :: RINGCAT1:13 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::) "holds"   (Bool  "("  (Bool (Set (Var "D")) "is"    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))))  ")" ))) ; 
 
theorem :: RINGCAT1:14 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H")) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is"    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Var "G")) "," (Set (Var "H"))))) ; 
 definitionlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); assume 
(Bool (Set (Const "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Const "H")))
 ; func  :::"Morphs":::  "(" "G" "," "H" ")"  ->    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" "G" "," "H" means :: RINGCAT1:def 14 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" "G" "," "H")  ")" )); end; 







:: deftheorem    defines :::"Morphs"::: RINGCAT1:def 14 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#l6_algstr_0 :::"Ring":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "H")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Var "G")) "," (Set (Var "H")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_ringcat1 :::"Morphs"::: )   "(" (Set (Var "G")) "," (Set (Var "H")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H")))  ")" ))  ")" ))); 
 definitionlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); let "M" be    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Const "G")) "," (Set (Const "H")); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "M" ->    ($#m1_ringcat1 :::"Morphism"::: )   "of" "G" "," "H"; end; registrationlet "G", "H" be   ($#l6_algstr_0 :::"Ring":::); let "M" be    ($#m4_ringcat1 :::"RingMorphism_DOMAIN"::: )   "of" (Set (Const "G")) "," (Set (Const "H")); 
cluster   ($#v2_ringcat1 :::"strict"::: )     ($#v3_ringcat1 :::"RingMorphism-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "M"; 
end; definitionlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; pred  :::"GO"::: "x" "," "y" means :: RINGCAT1:def 15 (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k3_xtuple_0 :::"]"::: ) )) & (Bool  "ex" (Set (Var "G")) "being"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Ring":::) "st"  (Bool  "("  (Bool "y"  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "G")))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "G")))) & (Bool (Set (Var "x5"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x6"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "G"))))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"GO"::: RINGCAT1:def 15 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xtuple_0 :::"["::: ) (Set  ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) ) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k3_xtuple_0 :::"]"::: ) )) & (Bool  "ex" (Set (Var "G")) "being"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Ring":::) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_vectsp_1 :::"comp"::: )  (Set (Var "G")))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "G")))) & (Bool (Set (Var "x5"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "x6"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "G"))))  ")" ))  ")" ))  ")" )); 
 
theorem :: RINGCAT1:15 (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set (Var "y1"))) & (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set (Var "y2")))) "holds"  (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))) ; 
 
theorem :: RINGCAT1:16 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::) (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "UN"))) & (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set   ($#k18_mod_2 :::"Z_3"::: )  ))  ")" ))) ; 
 definitionlet "UN" be   ($#m1_hidden :::"Universe":::); func  :::"RingObjects"::: "UN" ->    ($#m1_hidden :::"set"::: )   means :: RINGCAT1:def 16 (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "UN") & (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set (Var "y")))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"RingObjects"::: RINGCAT1:def 16 :  (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")))) "iff" (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "UN"))) & (Bool   ($#r2_ringcat1 :::"GO"::: )  (Set (Var "x")) "," (Set (Var "y")))  ")" ))  ")" ))  ")" ))); 
 
theorem :: RINGCAT1:17 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k18_mod_2 :::"Z_3"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN"))))) ; 
 registrationlet "UN" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k9_ringcat1 :::"RingObjects"::: )  "UN") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: RINGCAT1:18 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN"))) "holds"  (Bool (Set (Var "x")) "is"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Ring":::)))) ; 
 registrationlet "UN" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k9_ringcat1 :::"RingObjects"::: )  "UN") ->   ($#v4_ringcat1 :::"Ring_DOMAIN-like"::: )   ; 
end; definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); func  :::"Morphs"::: "V" ->   ($#m1_hidden :::"RingMorphism_DOMAIN":::) means :: RINGCAT1:def 17 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "G")) "," (Set (Var "H")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" "V" "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "H"))) & (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H")))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"Morphs"::: RINGCAT1:def 17 :  (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"RingMorphism_DOMAIN":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "G")) "," (Set (Var "H")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "H"))) & (Bool (Set (Var "x")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G")) "," (Set (Var "H")))  ")" ))  ")" ))  ")" ))); 
 definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); let "F" be    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Const "V"))); :: original: :::"dom"::: redefine func  :::"dom"::: "F" ->    ($#m2_ringcat1 :::"Element"::: )   "of" "V"; :: original: :::"cod"::: redefine func  :::"cod"::: "F" ->    ($#m2_ringcat1 :::"Element"::: )   "of" "V"; end; definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); let "G" be    ($#m2_ringcat1 :::"Element"::: )   "of" (Set (Const "V")); func  :::"ID"::: "G" ->   ($#v2_ringcat1 :::"strict"::: )     ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  "V") equals :: RINGCAT1:def 18 (Set   ($#k5_ringcat1 :::"ID"::: )  "G"); canceled; end; 






:: deftheorem    defines :::"ID"::: RINGCAT1:def 18 :  (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "G")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k13_ringcat1 :::"ID"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_ringcat1 :::"ID"::: )  (Set (Var "G")))))); 
 
:: deftheorem   RINGCAT1:def 19 :  canceled;  
 definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); func  :::"dom"::: "V" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  "V" ")" ) "," "V" means :: RINGCAT1:def 20 (Bool  "for" (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  "V") "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "f"))))); func  :::"cod"::: "V" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  "V" ")" ) "," "V" means :: RINGCAT1:def 21 (Bool  "for" (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  "V") "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f"))))); canceled; end; 










:: deftheorem    defines :::"dom"::: RINGCAT1:def 20 :  (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_ringcat1 :::"dom"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "f")))))  ")" ))); 
 
:: deftheorem    defines :::"cod"::: RINGCAT1:def 21 :  (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_ringcat1 :::"cod"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f")))))  ")" ))); 
 
:: deftheorem   RINGCAT1:def 22 :  canceled;  
 
theorem :: RINGCAT1:19 (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")))  "st" (Bool (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool  "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G2"))) & (Bool (Set (Var "G2"))  ($#r1_ringcat1 :::"<="::: )  (Set (Var "G3"))) & (Bool (Set (Var "g")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set (Var "f")) "is"    ($#m1_ringcat1 :::"Morphism"::: )   "of" (Set (Var "G1")) "," (Set (Var "G2")))  ")" )))) ; 
 
theorem :: RINGCAT1:20 (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")))  "st" (Bool (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")))))) ; 
 definitionlet "V" be   ($#m1_hidden :::"Ring_DOMAIN":::); func  :::"comp"::: "V" ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  "V" ")" ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  "V" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  "V" ")" ) means :: RINGCAT1:def 23 (Bool  "("  (Bool  "("   "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  "V") "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it)) "iff" (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f"))))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  "V")  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"comp"::: RINGCAT1:def 23 :  (Bool  "for" (Set (Var "V")) "being"   ($#m1_hidden :::"Ring_DOMAIN":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")) ")" ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_ringcat1 :::"comp"::: )  (Set (Var "V")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V"))) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b2")))) "iff" (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f"))))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "g")) "," (Set (Var "f")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set (Var "V")))  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f"))))  ")" )  ")" )  ")" ))); 
 definitionlet "UN" be   ($#m1_hidden :::"Universe":::); func  :::"RingCat"::: "UN" ->    ($#l1_cat_1 :::"CatStr"::: )   equals :: RINGCAT1:def 24 (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  "UN" ")" ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  "UN" ")" ) ")" ) "," (Set  "("  ($#k14_ringcat1 :::"dom"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  "UN" ")" ) ")" ) "," (Set  "("  ($#k15_ringcat1 :::"cod"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  "UN" ")" ) ")" ) "," (Set  "("  ($#k16_ringcat1 :::"comp"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  "UN" ")" ) ")" ) "#)" ); end; 





:: deftheorem    defines :::"RingCat"::: RINGCAT1:def 24 :  (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_cat_1 :::"CatStr"::: )  "(#"  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) "," (Set  "("  ($#k10_ringcat1 :::"Morphs"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" ) "," (Set  "("  ($#k14_ringcat1 :::"dom"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" ) "," (Set  "("  ($#k15_ringcat1 :::"cod"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" ) "," (Set  "("  ($#k16_ringcat1 :::"comp"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" ) "#)" ))); 
 registrationlet "UN" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k17_ringcat1 :::"RingCat"::: )  "UN") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_cat_1 :::"strict"::: )   ; 
end; 
theorem :: RINGCAT1:21 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )))) "iff" (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))  ")" ))) ; 
 
theorem :: RINGCAT1:22 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )  (Bool  "for" (Set (Var "f9")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )  (Bool  "for" (Set (Var "b9")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN"))) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_ringcat1 :::"strict"::: )     ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ))) & (Bool (Set (Var "f9")) "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )) & (Bool (Set (Var "b")) "is"   ($#v36_algstr_0 :::"strict"::: )     ($#m2_ringcat1 :::"Element"::: )   "of" (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")))) & (Bool (Set (Var "b9")) "is"   ($#m1_subset_1 :::"Object":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" ))  ")" )))))) ; 
 
theorem :: RINGCAT1:23 canceled; 
 
theorem :: RINGCAT1:24 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )  (Bool  "for" (Set (Var "f9")) "," (Set (Var "g9")) "being"    ($#m3_ringcat1 :::"Element"::: )   "of" (Set   ($#k10_ringcat1 :::"Morphs"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "f9"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "g9")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "implies" (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g9")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f9"))))  ")"  &  "("  (Bool (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g9")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f9"))))) "implies" (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))  ")"  &  "("  (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "implies" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g9")) "," (Set (Var "f9")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k16_ringcat1 :::"comp"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" )))  ")"  &  "("  (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "g9")) "," (Set (Var "f9")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "("  ($#k16_ringcat1 :::"comp"::: )  (Set  "("  ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")) ")" ) ")" )))) "implies" (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))  ")"  &  "("  (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "g"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g9"))  ($#k6_ringcat1 :::"*"::: )  (Set (Var "f9"))))  ")"  &  "("  (Bool (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g"))))) "implies" (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "f9")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g9"))))  ")"  &  "("  (Bool (Bool (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "f9")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_ringcat1 :::"dom"::: )  (Set (Var "g9"))))) "implies" (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g"))))  ")"  &  "("  (Bool (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g"))))) "implies" (Bool (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f9")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "g9"))))  ")"  &  "("  (Bool (Bool (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "f9")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ringcat1 :::"cod"::: )  (Set (Var "g9"))))) "implies" (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g"))))  ")"   ")" )))) ; 
 registrationlet "UN" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k17_ringcat1 :::"RingCat"::: )  "UN") ->   ($#v2_cat_1 :::"Category-like"::: )     ($#v3_cat_1 :::"transitive"::: )     ($#v4_cat_1 :::"associative"::: )     ($#v5_cat_1 :::"reflexive"::: )   ; 
end; registrationlet "UN" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k17_ringcat1 :::"RingCat"::: )  "UN") ->   ($#v6_cat_1 :::"with_identities"::: )   ; 
end; 
theorem :: RINGCAT1:25 (Bool  "for" (Set (Var "UN")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set  "("  ($#k17_ringcat1 :::"RingCat"::: )  (Set (Var "UN")) ")" )  (Bool  "for" (Set (Var "aa")) "being"    ($#m2_ringcat1 :::"Element"::: )   "of" (Set   ($#k9_ringcat1 :::"RingObjects"::: )  (Set (Var "UN")))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "aa")))) "holds"  (Bool (Set   ($#k4_cat_1 :::"id"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k13_ringcat1 :::"ID"::: )  (Set (Var "aa"))))))) ;