:: AUTGROUP  semantic presentation begin  




















theorem :: AUTGROUP:1 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "H")) "being"    ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "b")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")))) "holds"  (Bool (Set (Set (Var "b"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "a")))  ($#r1_struct_0 :::"in"::: )  (Set (Var "H")))  ")" ) "iff" (Bool (Set (Var "H")) "is"   ($#v1_group_3 :::"normal"::: )  )  ")" ))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); func  :::"Aut"::: "G" ->    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") means :: AUTGROUP:def 1 (Bool  "("  (Bool  "("   "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" it "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "G")  ")" ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "G" "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "h")) "is"   ($#v2_funct_2 :::"onto"::: )  )  ")" )  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"Aut"::: AUTGROUP:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set (Var "b2")) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")))  ")" ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "h")) "is"   ($#v2_funct_2 :::"onto"::: )  )  ")" )  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: AUTGROUP:2 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" ))) ; 
 
theorem :: AUTGROUP:3 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))))) ; 
 
theorem :: AUTGROUP:4 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))) "iff" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )  ")" ))) ; 
 
theorem :: AUTGROUP:5 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G"))))) ; 
 
theorem :: AUTGROUP:6 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))))) ; 
 
theorem :: AUTGROUP:7 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2"))) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); func  :::"AutComp"::: "G" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_autgroup :::"Aut"::: )  "G" ")" ) means :: AUTGROUP:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  "G") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "y"))))); end; 





:: deftheorem    defines :::"AutComp"::: AUTGROUP:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_autgroup :::"AutComp"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "y")))))  ")" ))); 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); func  :::"AutGroup"::: "G" ->   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) equals :: AUTGROUP:def 3 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k1_autgroup :::"Aut"::: )  "G" ")" ) "," (Set  "("  ($#k2_autgroup :::"AutComp"::: )  "G" ")" ) "#)" ); end; 





:: deftheorem    defines :::"AutGroup"::: AUTGROUP:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k3_autgroup :::"AutGroup"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")) ")" ) "," (Set  "("  ($#k2_autgroup :::"AutComp"::: )  (Set (Var "G")) ")" ) "#)" ))); 
 
theorem :: AUTGROUP:8 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_autgroup :::"AutGroup"::: )  (Set (Var "G")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g"))))))) ; 
 
theorem :: AUTGROUP:9 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k3_autgroup :::"AutGroup"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: AUTGROUP:10 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_autgroup :::"AutGroup"::: )  (Set (Var "G")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_group_1 :::"""::: )  ))))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); func  :::"InnAut"::: "G" ->    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") means :: AUTGROUP:def 4 (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "a"))))))  ")" )); end; 





:: deftheorem    defines :::"InnAut"::: AUTGROUP:def 4 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "a"))))))  ")" ))  ")" ))); 
 
theorem :: AUTGROUP:11 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) ")" ))) ; 
 
theorem :: AUTGROUP:12 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Var "f")) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G")))))) ; 
 
theorem :: AUTGROUP:13 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_autgroup :::"Aut"::: )  (Set (Var "G"))))) ; 
 
theorem :: AUTGROUP:14 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set  "("  ($#k2_autgroup :::"AutComp"::: )  (Set (Var "G")) ")" )  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))))) ; 
 
theorem :: AUTGROUP:15 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))))) ; 
 
theorem :: AUTGROUP:16 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))))) ; 
 
theorem :: AUTGROUP:17 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g"))) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); func  :::"InnAutGroup"::: "G" ->   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set   ($#k3_autgroup :::"AutGroup"::: )  "G") means :: AUTGROUP:def 5 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_autgroup :::"InnAut"::: )  "G")); end; 





:: deftheorem    defines :::"InnAutGroup"::: AUTGROUP:def 5 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#v1_group_3 :::"normal"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set   ($#k3_autgroup :::"AutGroup"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))))  ")" ))); 
 
theorem :: AUTGROUP:18 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g"))))))) ; 
 
theorem :: AUTGROUP:19 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: AUTGROUP:20 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_group_1 :::"""::: )  ))))) ; 
 definitionlet "G" be   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::); let "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func  :::"Conjugate"::: "b" ->    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  "G") means :: AUTGROUP:def 6 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_group_3 :::"|^"::: )  "b"))); end; 






:: deftheorem    defines :::"Conjugate"::: AUTGROUP:def 6 :  (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "b")))) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "b")))))  ")" )))); 
 
theorem :: AUTGROUP:21 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set  "(" (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "b")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: AUTGROUP:22 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))))) ; 
 
theorem :: AUTGROUP:23 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: AUTGROUP:24 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ))))) ; 
 
theorem :: AUTGROUP:25 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ))))) ; 
 
theorem :: AUTGROUP:26 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set  "(" (Set (Var "a"))  ($#k2_group_1 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" )  ($#k2_funct_1 :::"""::: )  )))) ; 
 
theorem :: AUTGROUP:27 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")))) & (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_autgroup :::"Conjugate"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: AUTGROUP:28 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k4_autgroup :::"InnAut"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set (Set  "("  ($#k6_autgroup :::"Conjugate"::: )  (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "G")) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))  ")" ))) ; 
 
theorem :: AUTGROUP:29 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G"))) "," (Set (Set (Var "G"))  ($#k5_group_6 :::"./."::: )  (Set  "("  ($#k10_group_5 :::"center"::: )  (Set (Var "G")) ")" ))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ; 
 
theorem :: AUTGROUP:30 (Bool  "for" (Set (Var "G")) "being"   ($#v15_algstr_0 :::"strict"::: )    ($#l3_algstr_0 :::"Group":::)  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v5_group_1 :::"commutative"::: )    ($#l3_algstr_0 :::"Group":::))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k5_autgroup :::"InnAutGroup"::: )  (Set (Var "G")) ")" ))))) ;