:: GRCAT_1 semantic presentation begin theorem :: GRCAT_1:1 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "u3")) "," (Set (Var "u4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "UN")) "holds" (Bool "(" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "u3")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "u3")) "," (Set (Var "u4")) ($#k6_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) ")" ))) ; theorem :: GRCAT_1:2 (Bool "(" (Bool (Set (Set ($#k9_funct_5 :::"op2"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set ($#k8_funct_5 :::"op1"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_funct_5 :::"op0"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: GRCAT_1:3 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k9_funct_5 :::"op2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) & (Bool (Set ($#k8_funct_5 :::"op1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "UN"))) ")" )) ; registration cluster (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) -> ($#v2_midsp_2 :::"midpoint_operator"::: ) ; end; theorem :: GRCAT_1:4 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "C"))); func :::"Morphs"::: "O" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") equals :: GRCAT_1:def 1 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) where a, b "is" ($#m1_subset_1 :::"Object":::) "of" "C" : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "O") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "O") ")" ) "}" ); end; :: deftheorem defines :::"Morphs"::: GRCAT_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k1_grcat_1 :::"Morphs"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) where a, b "is" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "O"))) ")" ) "}" )))); registrationlet "C" be ($#l1_cat_1 :::"Category":::); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "C"))); cluster (Set ($#k1_grcat_1 :::"Morphs"::: ) "O") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "C"))); func :::"dom"::: "O" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) "," "O" equals :: GRCAT_1:def 2 (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" )); func :::"cod"::: "O" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) "," "O" equals :: GRCAT_1:def 3 (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" )); func :::"comp"::: "O" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) "," (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) equals :: GRCAT_1:def 4 (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C") ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" )); canceled; end; :: deftheorem defines :::"dom"::: GRCAT_1:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k2_grcat_1 :::"dom"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) (Set (Var "O")) ")" ))))); :: deftheorem defines :::"cod"::: GRCAT_1:def 3 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k3_grcat_1 :::"cod"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) (Set (Var "O")) ")" ))))); :: deftheorem defines :::"comp"::: GRCAT_1:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k4_grcat_1 :::"comp"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k1_realset1 :::"||"::: ) (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) (Set (Var "O")) ")" ))))); :: deftheorem GRCAT_1:def 5 : canceled; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "C"))); func :::"cat"::: "O" -> ($#m3_cat_2 :::"Subcategory"::: ) "of" "C" equals :: GRCAT_1:def 6 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" "O" "," (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) "O" ")" ) "," (Set "(" ($#k2_grcat_1 :::"dom"::: ) "O" ")" ) "," (Set "(" ($#k3_grcat_1 :::"cod"::: ) "O" ")" ) "," (Set "(" ($#k4_grcat_1 :::"comp"::: ) "O" ")" ) "#)" ); end; :: deftheorem defines :::"cat"::: GRCAT_1:def 6 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k5_grcat_1 :::"cat"::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set (Var "O")) "," (Set "(" ($#k1_grcat_1 :::"Morphs"::: ) (Set (Var "O")) ")" ) "," (Set "(" ($#k2_grcat_1 :::"dom"::: ) (Set (Var "O")) ")" ) "," (Set "(" ($#k3_grcat_1 :::"cod"::: ) (Set (Var "O")) ")" ) "," (Set "(" ($#k4_grcat_1 :::"comp"::: ) (Set (Var "O")) ")" ) "#)" )))); registrationlet "C" be ($#l1_cat_1 :::"Category":::); let "O" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "C"))); cluster (Set ($#k5_grcat_1 :::"cat"::: ) "O") -> ($#v1_cat_1 :::"strict"::: ) ; end; theorem :: GRCAT_1:5 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_grcat_1 :::"cat"::: ) (Set (Var "O")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "O"))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; func :::"ZeroMap"::: "(" "G" "," "H" ")" -> ($#m1_subset_1 :::"Function":::) "of" "G" "," "H" equals :: GRCAT_1:def 7 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "H" ")" )); end; :: deftheorem defines :::"ZeroMap"::: GRCAT_1:def 7 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k6_grcat_1 :::"ZeroMap"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "H")) ")" ))))); theorem :: GRCAT_1:6 (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) )) ($#r1_funct_2 :::"="::: ) (Set ($#k8_funct_5 :::"op1"::: ) )) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k6_grcat_1 :::"ZeroMap"::: ) "(" "G" "," "H" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; end; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#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 :::":]"::: ) )); end; theorem :: GRCAT_1:7 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) (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" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "g")) "is" ($#v13_vectsp_1 :::"additive"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v13_vectsp_1 :::"additive"::: ) )))) ; registrationlet "G1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "G2", "G3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f" be ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G1")) "," (Set (Const "G2")); let "g" be ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G2")) "," (Set (Const "G3")); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v13_vectsp_1 :::"additive"::: ) for ($#m1_subset_1 :::"Function":::) "of" "G1" "," "G3"; end; definitionattr "c1" is :::"strict"::: ; struct :::"GroupMorphismStr"::: -> ; aggr :::"GroupMorphismStr":::(# :::"Source":::, :::"Target":::, :::"Fun"::: #) -> ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; sel :::"Source"::: "c1" -> ($#l2_algstr_0 :::"AddGroup":::); sel :::"Target"::: "c1" -> ($#l2_algstr_0 :::"AddGroup":::); sel :::"Fun"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" "c1") "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" "c1"); end; definitioncanceled; let "f" be ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; func :::"dom"::: "f" -> ($#l2_algstr_0 :::"AddGroup":::) equals :: GRCAT_1:def 9 (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" "f"); func :::"cod"::: "f" -> ($#l2_algstr_0 :::"AddGroup":::) equals :: GRCAT_1:def 10 (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" "f"); end; :: deftheorem GRCAT_1:def 8 : canceled; :: deftheorem defines :::"dom"::: GRCAT_1:def 9 : (Bool "for" (Set (Var "f")) "being" ($#l1_grcat_1 :::"GroupMorphismStr"::: ) "holds" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" (Set (Var "f"))))); :: deftheorem defines :::"cod"::: GRCAT_1:def 10 : (Bool "for" (Set (Var "f")) "being" ($#l1_grcat_1 :::"GroupMorphismStr"::: ) "holds" (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" (Set (Var "f"))))); definitionlet "f" be ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; func :::"fun"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_grcat_1 :::"dom"::: ) "f" ")" ) "," (Set "(" ($#k8_grcat_1 :::"cod"::: ) "f" ")" ) equals :: GRCAT_1:def 11 (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" "f"); end; :: deftheorem defines :::"fun"::: GRCAT_1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#l1_grcat_1 :::"GroupMorphismStr"::: ) "holds" (Bool (Set ($#k9_grcat_1 :::"fun"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" (Set (Var "f"))))); theorem :: GRCAT_1:8 (Bool "for" (Set (Var "f")) "being" ($#l1_grcat_1 :::"GroupMorphismStr"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f0")) "#)" ))) "holds" (Bool "(" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G1"))) & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) & (Bool (Set ($#k9_grcat_1 :::"fun"::: ) (Set (Var "f"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f0"))) ")" )))) ; definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); func :::"ZERO"::: "(" "G" "," "H" ")" -> ($#l1_grcat_1 :::"GroupMorphismStr"::: ) equals :: GRCAT_1:def 12 (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" "G" "," "H" "," (Set "(" ($#k6_grcat_1 :::"ZeroMap"::: ) "(" "G" "," "H" ")" ")" ) "#)" ); end; :: deftheorem defines :::"ZERO"::: GRCAT_1:def 12 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) "holds" (Bool (Set ($#k10_grcat_1 :::"ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set "(" ($#k6_grcat_1 :::"ZeroMap"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ")" ) "#)" ))); registrationlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); cluster (Set ($#k10_grcat_1 :::"ZERO"::: ) "(" "G" "," "H" ")" ) -> ($#v1_grcat_1 :::"strict"::: ) ; end; definitionlet "IT" be ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; attr "IT" is :::"GroupMorphism-like"::: means :: GRCAT_1:def 13 (Bool (Set ($#k9_grcat_1 :::"fun"::: ) "IT") "is" ($#v13_vectsp_1 :::"additive"::: ) ); end; :: deftheorem defines :::"GroupMorphism-like"::: GRCAT_1:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#l1_grcat_1 :::"GroupMorphismStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_grcat_1 :::"GroupMorphism-like"::: ) ) "iff" (Bool (Set ($#k9_grcat_1 :::"fun"::: ) (Set (Var "IT"))) "is" ($#v13_vectsp_1 :::"additive"::: ) ) ")" )); registration cluster ($#v1_grcat_1 :::"strict"::: ) ($#v2_grcat_1 :::"GroupMorphism-like"::: ) for ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; end; definitionmode GroupMorphism is ($#v2_grcat_1 :::"GroupMorphism-like"::: ) ($#l1_grcat_1 :::"GroupMorphismStr"::: ) ; end; theorem :: GRCAT_1:9 (Bool "for" (Set (Var "F")) "being" ($#l1_grcat_1 :::"GroupMorphism":::) "holds" (Bool (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" (Set (Var "F"))) "is" ($#v13_vectsp_1 :::"additive"::: ) )) ; registrationlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); cluster (Set ($#k10_grcat_1 :::"ZERO"::: ) "(" "G" "," "H" ")" ) -> ($#v2_grcat_1 :::"GroupMorphism-like"::: ) ; end; definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); mode :::"Morphism"::: "of" "G" "," "H" -> ($#l1_grcat_1 :::"GroupMorphism":::) means :: GRCAT_1:def 14 (Bool "(" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "G") & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) it) ($#r1_hidden :::"="::: ) "H") ")" ); end; :: deftheorem defines :::"Morphism"::: GRCAT_1:def 14 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "b3")) "being" ($#l1_grcat_1 :::"GroupMorphism":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "(" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) ")" ) ")" ))); registrationlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); cluster ($#v1_grcat_1 :::"strict"::: ) ($#v2_grcat_1 :::"GroupMorphism-like"::: ) for ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "H"; end; theorem :: GRCAT_1:10 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphismStr"::: ) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) & (Bool (Set ($#k9_grcat_1 :::"fun"::: ) (Set (Var "f"))) "is" ($#v13_vectsp_1 :::"additive"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))))) ; theorem :: GRCAT_1:11 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) )) "holds" (Bool (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" ) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "G") -> ($#v13_vectsp_1 :::"additive"::: ) ; end; definitionlet "G" be ($#l2_algstr_0 :::"AddGroup":::); func :::"ID"::: "G" -> ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "G" equals :: GRCAT_1:def 15 (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" "G" "," "G" "," (Set "(" ($#k3_struct_0 :::"id"::: ) "G" ")" ) "#)" ); end; :: deftheorem defines :::"ID"::: GRCAT_1:def 15 : (Bool "for" (Set (Var "G")) "being" ($#l2_algstr_0 :::"AddGroup":::) "holds" (Bool (Set ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "G")) "," (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "G")) ")" ) "#)" ))); registrationlet "G" be ($#l2_algstr_0 :::"AddGroup":::); cluster (Set ($#k11_grcat_1 :::"ID"::: ) "G") -> ($#v1_grcat_1 :::"strict"::: ) ; end; definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); :: original: :::"ZERO"::: redefine func :::"ZERO"::: "(" "G" "," "H" ")" -> ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "H"; end; theorem :: GRCAT_1:12 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "F")) "being" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool "(" (Bool (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" (Set (Var "F"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) ")" )))) ; theorem :: GRCAT_1:13 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "F")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" ))))) ; theorem :: GRCAT_1:14 (Bool "for" (Set (Var "F")) "being" ($#l1_grcat_1 :::"GroupMorphism":::) (Bool "ex" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) "st" (Bool (Set (Var "F")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))))) ; theorem :: GRCAT_1:15 (Bool "for" (Set (Var "F")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) (Bool "ex" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::)(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_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "f")) "#)" )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) ")" )))) ; theorem :: GRCAT_1:16 (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set (Var "f")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2"))) ")" ))) ; definitionlet "G", "F" be ($#l1_grcat_1 :::"GroupMorphism":::); assume (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Const "G"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Const "F")))) ; func "G" :::"*"::: "F" -> ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) means :: GRCAT_1:def 16 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::) (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_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" "G") "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" "G") "," (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" "G") "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" "F") "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" "F") "," (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" "F") "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))); end; :: deftheorem defines :::"*"::: GRCAT_1:def 16 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::) (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_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set "the" ($#u1_grcat_1 :::"Source"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_grcat_1 :::"Target"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u3_grcat_1 :::"Fun"::: ) "of" (Set (Var "F"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))) ")" ))); theorem :: GRCAT_1:17 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "G")) "being" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "F")) "being" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "G")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "F"))) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G3")))))) ; definitionlet "G1", "G2", "G3" be ($#l2_algstr_0 :::"AddGroup":::); let "G" be ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Const "G2")) "," (Set (Const "G3")); let "F" be ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); :: original: :::"*"::: redefine func "G" :::"*"::: "F" -> ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" "G1" "," "G3"; end; theorem :: GRCAT_1:18 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "G")) "being" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "F")) "being" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (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 (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g")) "#)" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f")) "#)" ))) "holds" (Bool (Set (Set (Var "G")) ($#k14_grcat_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))))) ; theorem :: GRCAT_1:19 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l2_algstr_0 :::"AddGroup":::)(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_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "f0")) "#)" )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "g0")) "#)" )) & (Bool (Set (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#g1_grcat_1 :::"GroupMorphismStr"::: ) "(#" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set "(" (Set (Var "g0")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f0")) ")" ) "#)" )) ")" ))))) ; theorem :: GRCAT_1:20 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set "(" (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "g")))) ")" )) ; theorem :: GRCAT_1:21 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "," (Set (Var "G4")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "g")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "h")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G3")) "," (Set (Var "G4")) "holds" (Bool (Set (Set (Var "h")) ($#k14_grcat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k14_grcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k14_grcat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k14_grcat_1 :::"*"::: ) (Set (Var "f")))))))) ; theorem :: GRCAT_1:22 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "g")))) & (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k13_grcat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f"))))) ; theorem :: GRCAT_1:23 (Bool "for" (Set (Var "G")) "being" ($#l2_algstr_0 :::"AddGroup":::) "holds" (Bool "(" (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set "(" ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set "(" ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool "(" "for" (Set (Var "f")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k8_grcat_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set "(" ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G")) ")" ) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "st" (Bool (Bool (Set ($#k7_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set "(" ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" )) ; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"Group_DOMAIN-like"::: means :: GRCAT_1:def 17 (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" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AddGroup":::))); end; :: deftheorem defines :::"Group_DOMAIN-like"::: GRCAT_1:def 17 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_grcat_1 :::"Group_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" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AddGroup":::))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_grcat_1 :::"Group_DOMAIN-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode Group_DOMAIN is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_grcat_1 :::"Group_DOMAIN-like"::: ) ($#m1_hidden :::"set"::: ) ; end; definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "V" -> ($#l2_algstr_0 :::"AddGroup":::); end; registrationlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "V"; end; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"GroupMorphism_DOMAIN-like"::: means :: GRCAT_1:def 18 (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" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::))); end; :: deftheorem defines :::"GroupMorphism_DOMAIN-like"::: GRCAT_1:def 18 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_grcat_1 :::"GroupMorphism_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" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_grcat_1 :::"GroupMorphism_DOMAIN-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode GroupMorphism_DOMAIN is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_grcat_1 :::"GroupMorphism_DOMAIN-like"::: ) ($#m1_hidden :::"set"::: ) ; end; definitionlet "M" be ($#m1_hidden :::"GroupMorphism_DOMAIN":::); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "M" -> ($#l1_grcat_1 :::"GroupMorphism":::); end; registrationlet "M" be ($#m1_hidden :::"GroupMorphism_DOMAIN":::); cluster ($#v1_grcat_1 :::"strict"::: ) ($#v2_grcat_1 :::"GroupMorphism-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "M"; end; theorem :: GRCAT_1:24 (Bool "for" (Set (Var "f")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#l1_grcat_1 :::"GroupMorphism":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"GroupMorphism_DOMAIN":::))) ; definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); mode :::"GroupMorphism_DOMAIN"::: "of" "G" "," "H" -> ($#m1_hidden :::"GroupMorphism_DOMAIN":::) means :: GRCAT_1:def 19 (Bool "for" (Set (Var "x")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "H")); end; :: deftheorem defines :::"GroupMorphism_DOMAIN"::: GRCAT_1:def 19 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"GroupMorphism_DOMAIN":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set (Var "b3")) "holds" (Bool (Set (Var "x")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" ))); theorem :: GRCAT_1:25 (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" ($#l2_algstr_0 :::"AddGroup":::) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#m4_grcat_1 :::"GroupMorphism_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" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" ))) ; theorem :: GRCAT_1:26 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f")) "being" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))))) ; definitionlet "G", "H" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode :::"MapsSet"::: "of" "G" "," "H" -> ($#m1_hidden :::"set"::: ) means :: GRCAT_1:def 20 (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" ($#m1_subset_1 :::"Function":::) "of" "G" "," "H")); end; :: deftheorem defines :::"MapsSet"::: GRCAT_1:def 20 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m5_grcat_1 :::"MapsSet"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" ))); definitionlet "G", "H" be ($#l1_struct_0 :::"1-sorted"::: ) ; func :::"Maps"::: "(" "G" "," "H" ")" -> ($#m5_grcat_1 :::"MapsSet"::: ) "of" "G" "," "H" equals :: GRCAT_1:def 21 (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H") ")" ); end; :: deftheorem defines :::"Maps"::: GRCAT_1:def 21 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k15_grcat_1 :::"Maps"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ")" ))); registrationlet "G" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k15_grcat_1 :::"Maps"::: ) "(" "G" "," "H" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "G" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m5_grcat_1 :::"MapsSet"::: ) "of" "G" "," "H"; end; definitionlet "G" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "H" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m5_grcat_1 :::"MapsSet"::: ) "of" (Set (Const "G")) "," (Set (Const "H")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "M" -> ($#m1_subset_1 :::"Function":::) "of" "G" "," "H"; end; definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); func :::"Morphs"::: "(" "G" "," "H" ")" -> ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" "G" "," "H" means :: GRCAT_1:def 22 (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" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "H") ")" )); end; :: deftheorem defines :::"Morphs"::: GRCAT_1:def 22 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "b3")) "being" ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_grcat_1 :::"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" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) ")" )) ")" ))); definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); let "M" be ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" (Set (Const "G")) "," (Set (Const "H")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "M" -> ($#m1_grcat_1 :::"Morphism"::: ) "of" "G" "," "H"; end; registrationlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); let "M" be ($#m4_grcat_1 :::"GroupMorphism_DOMAIN"::: ) "of" (Set (Const "G")) "," (Set (Const "H")); cluster ($#v1_grcat_1 :::"strict"::: ) ($#v2_grcat_1 :::"GroupMorphism-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "M"; end; definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; pred :::"GO"::: "x" "," "y" means :: GRCAT_1:def 23 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )) & (Bool "ex" (Set (Var "G")) "being" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AddGroup":::) "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")))) ")" )) ")" )); end; :: deftheorem defines :::"GO"::: GRCAT_1:def 23 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_xtuple_0 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_xtuple_0 :::"]"::: ) )) & (Bool "ex" (Set (Var "G")) "being" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AddGroup":::) "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")))) ")" )) ")" )) ")" )); theorem :: GRCAT_1:27 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y1"))) & (Bool ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y2")))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) ; theorem :: GRCAT_1:28 (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 ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) )) ")" ))) ; definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"GroupObjects"::: "UN" -> ($#m1_hidden :::"set"::: ) means :: GRCAT_1:def 24 (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 ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" )); end; :: deftheorem defines :::"GroupObjects"::: GRCAT_1:def 24 : (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 ($#k17_grcat_1 :::"GroupObjects"::: ) (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 ($#r1_grcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" )) ")" ))); theorem :: GRCAT_1:29 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN"))))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k17_grcat_1 :::"GroupObjects"::: ) "UN") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GRCAT_1:30 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN"))) "holds" (Bool (Set (Var "x")) "is" ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AddGroup":::)))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k17_grcat_1 :::"GroupObjects"::: ) "UN") -> ($#v3_grcat_1 :::"Group_DOMAIN-like"::: ) ; end; definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); func :::"Morphs"::: "V" -> ($#m1_hidden :::"GroupMorphism_DOMAIN":::) means :: GRCAT_1:def 25 (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" ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" "V" "st" (Bool (Set (Var "x")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )); end; :: deftheorem defines :::"Morphs"::: GRCAT_1:def 25 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"GroupMorphism_DOMAIN":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_grcat_1 :::"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" ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )) ")" ))); definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); let "F" be ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Const "V"))); :: original: :::"dom"::: redefine func :::"dom"::: "F" -> ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" "V"; :: original: :::"cod"::: redefine func :::"cod"::: "F" -> ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" "V"; end; definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); let "G" be ($#m2_grcat_1 :::"Element"::: ) "of" (Set (Const "V")); func :::"ID"::: "G" -> ($#v1_grcat_1 :::"strict"::: ) ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) "V") equals :: GRCAT_1:def 26 (Set ($#k11_grcat_1 :::"ID"::: ) "G"); end; :: deftheorem defines :::"ID"::: GRCAT_1:def 26 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "G")) "being" ($#m2_grcat_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k21_grcat_1 :::"ID"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k11_grcat_1 :::"ID"::: ) (Set (Var "G")))))); definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); func :::"dom"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) "V" ")" ) "," "V" means :: GRCAT_1:def 27 (Bool "for" (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "f"))))); func :::"cod"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) "V" ")" ) "," "V" means :: GRCAT_1:def 28 (Bool "for" (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f"))))); end; :: deftheorem defines :::"dom"::: GRCAT_1:def 27 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k22_grcat_1 :::"dom"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "f"))))) ")" ))); :: deftheorem defines :::"cod"::: GRCAT_1:def 28 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k23_grcat_1 :::"cod"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f"))))) ")" ))); theorem :: GRCAT_1:31 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set (Var "f")) "is" ($#m1_grcat_1 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2"))) ")" )))) ; theorem :: GRCAT_1:32 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#m1_hidden :::"Group_DOMAIN":::); func :::"comp"::: "V" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) "V" ")" ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) "V" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) "V" ")" ) means :: GRCAT_1:def 29 (Bool "(" (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) "V") "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) "V") "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f")))) ")" ) ")" ); end; :: deftheorem defines :::"comp"::: GRCAT_1:def 29 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"Group_DOMAIN":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k24_grcat_1 :::"comp"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"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")) ($#k13_grcat_1 :::"*"::: ) (Set (Var "f")))) ")" ) ")" ) ")" ))); definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"GroupCat"::: "UN" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: GRCAT_1:def 30 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) "UN" ")" ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) "UN" ")" ) ")" ) "," (Set "(" ($#k22_grcat_1 :::"dom"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) "UN" ")" ) ")" ) "," (Set "(" ($#k23_grcat_1 :::"cod"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) "UN" ")" ) ")" ) "," (Set "(" ($#k24_grcat_1 :::"comp"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) "UN" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"GroupCat"::: GRCAT_1:def 30 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN"))) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) "," (Set "(" ($#k18_grcat_1 :::"Morphs"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) ")" ) "," (Set "(" ($#k22_grcat_1 :::"dom"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) ")" ) "," (Set "(" ($#k23_grcat_1 :::"cod"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) ")" ) "," (Set "(" ($#k24_grcat_1 :::"comp"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) ")" ) "#)" ))); registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k25_grcat_1 :::"GroupCat"::: ) "UN") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ; end; theorem :: GRCAT_1:33 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" )))) "iff" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" ))) ; theorem :: GRCAT_1:34 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) (Bool "for" (Set (Var "f9")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" )) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) (Bool "for" (Set (Var "b9")) "being" ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_grcat_1 :::"strict"::: ) ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ))) & (Bool (Set (Var "f9")) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" )) & (Bool (Set (Var "b")) "is" ($#v8_algstr_0 :::"strict"::: ) ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")))) & (Bool (Set (Var "b9")) "is" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" )) ")" )))))) ; theorem :: GRCAT_1:35 canceled; theorem :: GRCAT_1:36 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) (Bool "for" (Set (Var "f9")) "," (Set (Var "g9")) "being" ($#m3_grcat_1 :::"Element"::: ) "of" (Set ($#k18_grcat_1 :::"Morphs"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (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 ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g9"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f9")))) ")" & "(" (Bool (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g9"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"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 ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k24_grcat_1 :::"comp"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g9")) "," (Set (Var "f9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k24_grcat_1 :::"comp"::: ) (Set "(" ($#k17_grcat_1 :::"GroupObjects"::: ) (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")) ($#k13_grcat_1 :::"*"::: ) (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 ($#k19_grcat_1 :::"dom"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "g9")))) ")" & "(" (Bool (Bool (Set ($#k19_grcat_1 :::"dom"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k19_grcat_1 :::"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 ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "g9")))) ")" & "(" (Bool (Bool (Set ($#k20_grcat_1 :::"cod"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k20_grcat_1 :::"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 ($#k25_grcat_1 :::"GroupCat"::: ) "UN") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v5_cat_1 :::"reflexive"::: ) ; end; registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k25_grcat_1 :::"GroupCat"::: ) "UN") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v6_cat_1 :::"with_identities"::: ) ; end; definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"AbGroupObjects"::: "UN" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) "UN" ")" )) equals :: GRCAT_1:def 31 "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) "UN" ")" ) : (Bool "ex" (Set (Var "H")) "being" ($#l2_algstr_0 :::"AbGroup":::) "st" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "}" ; end; :: deftheorem defines :::"AbGroupObjects"::: GRCAT_1:def 31 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k26_grcat_1 :::"AbGroupObjects"::: ) (Set (Var "UN"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) : (Bool "ex" (Set (Var "H")) "being" ($#l2_algstr_0 :::"AbGroup":::) "st" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "}" )); theorem :: GRCAT_1:37 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k26_grcat_1 :::"AbGroupObjects"::: ) (Set (Var "UN"))))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k26_grcat_1 :::"AbGroupObjects"::: ) "UN") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"AbGroupCat"::: "UN" -> ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set ($#k25_grcat_1 :::"GroupCat"::: ) "UN") equals :: GRCAT_1:def 32 (Set ($#k5_grcat_1 :::"cat"::: ) (Set "(" ($#k26_grcat_1 :::"AbGroupObjects"::: ) "UN" ")" )); end; :: deftheorem defines :::"AbGroupCat"::: GRCAT_1:def 32 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k27_grcat_1 :::"AbGroupCat"::: ) (Set (Var "UN"))) ($#r1_hidden :::"="::: ) (Set ($#k5_grcat_1 :::"cat"::: ) (Set "(" ($#k26_grcat_1 :::"AbGroupObjects"::: ) (Set (Var "UN")) ")" )))); registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k27_grcat_1 :::"AbGroupCat"::: ) "UN") -> ($#v1_cat_1 :::"strict"::: ) ; end; theorem :: GRCAT_1:38 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k27_grcat_1 :::"AbGroupCat"::: ) (Set (Var "UN")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k26_grcat_1 :::"AbGroupObjects"::: ) (Set (Var "UN"))))) ; definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"MidOpGroupObjects"::: "UN" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k27_grcat_1 :::"AbGroupCat"::: ) "UN" ")" )) equals :: GRCAT_1:def 33 "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k27_grcat_1 :::"AbGroupCat"::: ) "UN" ")" ) : (Bool "ex" (Set (Var "H")) "being" ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"AbGroup":::) "st" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "}" ; end; :: deftheorem defines :::"MidOpGroupObjects"::: GRCAT_1:def 33 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) (Set (Var "UN"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "G")) where G "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k27_grcat_1 :::"AbGroupCat"::: ) (Set (Var "UN")) ")" ) : (Bool "ex" (Set (Var "H")) "being" ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"AbGroup":::) "st" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "}" )); registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) "UN") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "UN" be ($#m1_hidden :::"Universe":::); func :::"MidOpGroupCat"::: "UN" -> ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set ($#k27_grcat_1 :::"AbGroupCat"::: ) "UN") equals :: GRCAT_1:def 34 (Set ($#k5_grcat_1 :::"cat"::: ) (Set "(" ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) "UN" ")" )); end; :: deftheorem defines :::"MidOpGroupCat"::: GRCAT_1:def 34 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k29_grcat_1 :::"MidOpGroupCat"::: ) (Set (Var "UN"))) ($#r1_hidden :::"="::: ) (Set ($#k5_grcat_1 :::"cat"::: ) (Set "(" ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) (Set (Var "UN")) ")" )))); registrationlet "UN" be ($#m1_hidden :::"Universe":::); cluster (Set ($#k29_grcat_1 :::"MidOpGroupCat"::: ) "UN") -> ($#v1_cat_1 :::"strict"::: ) ; end; theorem :: GRCAT_1:39 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k29_grcat_1 :::"MidOpGroupCat"::: ) (Set (Var "UN")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) (Set (Var "UN"))))) ; theorem :: GRCAT_1:40 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) "holds" (Bool (Set ($#k3_algstr_0 :::"Trivial-addLoopStr"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k28_grcat_1 :::"MidOpGroupObjects"::: ) (Set (Var "UN"))))) ; theorem :: GRCAT_1:41 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "T")))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "S")))) & (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))) ; theorem :: GRCAT_1:42 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k25_grcat_1 :::"GroupCat"::: ) (Set (Var "UN")) ")" ) (Bool "for" (Set (Var "aa")) "being" ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (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 ($#k21_grcat_1 :::"ID"::: ) (Set (Var "aa"))))))) ;