:: GROUP_1 semantic presentation begin definitionlet "IT" be ($#l3_algstr_0 :::"multMagma"::: ) ; attr "IT" is :::"unital"::: means :: GROUP_1:def 1 (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "e")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ))); attr "IT" is :::"Group-like"::: means :: GROUP_1:def 2 (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "e")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )) ")" ))); attr "IT" is :::"associative"::: means :: GROUP_1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" )))); end; :: deftheorem defines :::"unital"::: GROUP_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_group_1 :::"unital"::: ) ) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "e")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ))) ")" )); :: deftheorem defines :::"Group-like"::: GROUP_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_group_1 :::"Group-like"::: ) ) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "e")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )) ")" ))) ")" )); :: deftheorem defines :::"associative"::: GROUP_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_group_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" )))) ")" )); registration cluster ($#v2_group_1 :::"Group-like"::: ) -> ($#v1_group_1 :::"unital"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; definitionmode Group is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GROUP_1:1 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t")) ")" ))) ")" ) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set (Var "s1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Set (Var "t")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool "ex" (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Set (Var "s1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "s2")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" )) ")" )))) "holds" (Bool (Set (Var "S")) "is" ($#l3_algstr_0 :::"Group":::))) ; theorem :: GROUP_1:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Set (Set (Var "r")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Set (Set (Var "t")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_group_1 :::"associative"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_group_1 :::"Group-like"::: ) ) ")" )) ; theorem :: GROUP_1:3 (Bool "(" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "#)" ) "is" ($#v3_group_1 :::"associative"::: ) ) & (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "#)" ) "is" ($#v2_group_1 :::"Group-like"::: ) ) ")" ) ; definitionlet "G" be ($#l3_algstr_0 :::"multMagma"::: ) ; assume (Bool (Set (Const "G")) "is" ($#v1_group_1 :::"unital"::: ) ) ; func :::"1_"::: "G" -> ($#m1_subset_1 :::"Element":::) "of" "G" means :: GROUP_1:def 4 (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) it) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set it ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" )); end; :: deftheorem defines :::"1_"::: GROUP_1:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_group_1 :::"unital"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "b2")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" )) ")" ))); theorem :: GROUP_1:4 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "e")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ) ")" )) "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "h" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "h" :::"""::: -> ($#m1_subset_1 :::"Element":::) "of" "G" means :: GROUP_1:def 5 (Bool "(" (Bool (Set "h" ($#k6_algstr_0 :::"*"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G")) & (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "h") ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G")) ")" ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")) "st" (Bool (Bool (Set (Set (Var "b2")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Const "G")))) & (Bool (Set (Set (Var "b1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Const "G"))))) "holds" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Const "G")))) & (Bool (Set (Set (Var "b2")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Const "G")))) ")" )) ; end; :: deftheorem defines :::"""::: GROUP_1:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "b3")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ) ")" ))); theorem :: GROUP_1:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) )))) ; theorem :: GROUP_1:6 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "f")))) "or" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: GROUP_1:7 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) "or" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:8 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) ; theorem :: GROUP_1:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) ))) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: GROUP_1:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:11 canceled; theorem :: GROUP_1:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_1 :::"""::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) )) ")" ))) ; theorem :: GROUP_1:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) ")" ))) ; theorem :: GROUP_1:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ))) ")" ))) ; theorem :: GROUP_1:15 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: GROUP_1:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "f")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: GROUP_1:17 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ))))) ; theorem :: GROUP_1:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) "iff" (Bool (Set (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ))) ")" ))) ; theorem :: GROUP_1:19 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) "iff" (Bool (Set (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ))) ")" ))) ; theorem :: GROUP_1:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) "iff" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) ")" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"inverse_op"::: "G" -> ($#m1_subset_1 :::"UnOp":::) "of" "G" means :: GROUP_1:def 6 (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ))); end; :: deftheorem defines :::"inverse_op"::: GROUP_1:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ))) ")" ))); registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") -> ($#v2_binop_1 :::"associative"::: ) ; end; theorem :: GROUP_1:21 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))))) ; theorem :: GROUP_1:22 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) ; registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") -> ($#v1_setwiseo :::"having_a_unity"::: ) ; end; theorem :: GROUP_1:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "G") -> ($#v1_finseqop :::"having_an_inverseOp"::: ) ; end; theorem :: GROUP_1:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G")))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_group_1 :::"inverse_op"::: ) (Set (Var "G"))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; func :::"power"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") means :: GROUP_1:def 7 (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool "(" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set (Var "n")) ")" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) ")" ) ")" )); end; :: deftheorem defines :::"power"::: GROUP_1:def 7 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_group_1 :::"power"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set (Var "n")) ")" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) ")" ) ")" )) ")" ))); definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "i" be ($#m1_hidden :::"Integer":::); let "h" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "h" :::"|^"::: "i" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: GROUP_1:def 8 (Set (Set "(" ($#k4_group_1 :::"power"::: ) "G" ")" ) ($#k2_binop_1 :::"."::: ) "(" "h" "," (Set "(" ($#k1_int_2 :::"abs"::: ) "i" ")" ) ")" ) if (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) "i") otherwise (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) "G" ")" ) ($#k2_binop_1 :::"."::: ) "(" "h" "," (Set "(" ($#k1_int_2 :::"abs"::: ) "i" ")" ) ")" ")" ) ($#k2_group_1 :::"""::: ) ); end; :: deftheorem defines :::"|^"::: GROUP_1:def 8 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "implies" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "G")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "G")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ")" ")" ) ($#k2_group_1 :::"""::: ) )) ")" ")" )))); definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "n" be ($#m1_hidden :::"Nat":::); let "h" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); redefine func "h" :::"|^"::: "n" equals :: GROUP_1:def 9 (Set (Set "(" ($#k4_group_1 :::"power"::: ) "G" ")" ) ($#k1_binop_1 :::"."::: ) "(" "h" "," "n" ")" ); end; :: deftheorem defines :::"|^"::: GROUP_1:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "G")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "h")) "," (Set (Var "n")) ")" ))))); theorem :: GROUP_1:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "h"))))) ; theorem :: GROUP_1:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))))) ; theorem :: GROUP_1:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))))) ; theorem :: GROUP_1:29 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) "iff" (Bool (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ))) ; theorem :: GROUP_1:30 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_group_1 :::"""::: ) ))))) ; theorem :: GROUP_1:31 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:32 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_1 :::"""::: ) )))) ; theorem :: GROUP_1:33 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k20_binop_2 :::"+"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "j")) ")" )))))) ; theorem :: GROUP_1:34 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k20_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) & (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k20_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ))) ")" )))) ; theorem :: GROUP_1:35 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "i")) ($#k22_binop_2 :::"*"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "j"))))))) ; theorem :: GROUP_1:36 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k19_binop_2 :::"-"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k2_group_1 :::"""::: ) ))))) ; theorem :: GROUP_1:37 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k2_group_1 :::"""::: ) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k2_group_1 :::"""::: ) ))))) ; theorem :: GROUP_1:38 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: GROUP_1:39 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "j")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: GROUP_1:40 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g"))))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "h" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); attr "h" is :::"being_of_order_0"::: means :: GROUP_1:def 10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "h" ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G"))) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"being_of_order_0"::: GROUP_1:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v4_group_1 :::"being_of_order_0"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))); registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k1_group_1 :::"1_"::: ) "G") -> ($#~v4_group_1 "non" ($#v4_group_1 :::"being_of_order_0"::: ) ) ; end; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "h" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"ord"::: "h" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GROUP_1:def 11 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) if (Bool "h" "is" ($#v4_group_1 :::"being_of_order_0"::: ) ) otherwise (Bool "(" (Bool (Set "h" ($#k5_group_1 :::"|^"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G")) & (Bool it ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "h" ($#k5_group_1 :::"|^"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "G")) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) ")" ); end; :: deftheorem defines :::"ord"::: GROUP_1:def 11 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "h")) "is" ($#v4_group_1 :::"being_of_order_0"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "h")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "h")) "is" ($#v4_group_1 :::"being_of_order_0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "h")))) "iff" (Bool "(" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) ")" ) ")" ) ")" ")" )))); theorem :: GROUP_1:41 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set "(" ($#k6_group_1 :::"ord"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:42 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: GROUP_1:43 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_1:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "h"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "n")))))) ; definitionlet "G" be ($#v8_struct_0 :::"finite"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; :: original: :::"card"::: redefine func :::"card"::: "G" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: GROUP_1:45 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ; definitionlet "IT" be ($#l3_algstr_0 :::"multMagma"::: ) ; attr "IT" is :::"commutative"::: means :: GROUP_1:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"commutative"::: GROUP_1:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_group_1 :::"commutative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; definitionlet "FS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FS")); :: original: :::"*"::: redefine func "x" :::"*"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "FS"); commutativity (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FS")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) ; end; theorem :: GROUP_1:46 (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "#)" ) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) ; theorem :: GROUP_1:47 (Bool "for" (Set (Var "A")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ))))) ; theorem :: GROUP_1:48 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "A")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" )))))) ; theorem :: GROUP_1:49 (Bool "for" (Set (Var "A")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "A")) ")" ) "#)" ) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "A")) ")" ) "#)" ) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "A")) ")" ) "#)" ) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "A")) ")" ) "#)" ) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) ")" )) ; begin theorem :: GROUP_1:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: GROUP_1:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))))) ; theorem :: GROUP_1:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "n")) ")" ")" )))))) ; definitionlet "G", "H" be ($#l3_algstr_0 :::"multMagma"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G")) "," (Set (Const "H")); attr "IT" is :::"unity-preserving"::: means :: GROUP_1:def 13 (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "G" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "H")); end; :: deftheorem defines :::"unity-preserving"::: GROUP_1:def 13 : (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_group_1 :::"unity-preserving"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "H")))) ")" )));