:: WEDDWITT  semantic presentation begin  
theorem :: WEDDWITT:1 (Bool  "for" (Set (Var "a")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Set (Var "q"))  ($#k2_newton :::"|^"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: WEDDWITT:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k2_newton :::"|^"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_nat_1 :::"*"::: )  (Set  "(" (Set (Var "k"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "r")) ")" ) ")" ))))) ; 
 
theorem :: WEDDWITT:3 (Bool  "for" (Set (Var "q")) "," (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "a")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "q"))  ($#k13_newton :::"|^"::: )  (Set (Var "b")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))) "holds"  (Bool (Set (Var "a"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "b")))) ; 
 
theorem :: WEDDWITT:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "n")) "," (Set (Var "q")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))) ; 
 
theorem :: WEDDWITT:5 (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "j"))))  ")" )) "holds"  (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set (Var "f")))))) ; 
 
theorem :: WEDDWITT:6 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set (Var "c")))))))) ; 
 begin  registrationlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); 
cluster (Set   ($#k10_group_5 :::"center"::: )  "G") ->   ($#v8_struct_0 :::"finite"::: )   ; 
end; definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func  :::"Centralizer"::: "a" ->   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" "G" means :: WEDDWITT:def 1 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "b")) where b "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set "a"  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  "a"))  "}"  ); end; 






:: deftheorem    defines :::"Centralizer"::: WEDDWITT:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "a")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "b")) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))  "}"  )  ")" )))); 
 registrationlet "G" be   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); 
cluster (Set   ($#k1_weddwitt :::"Centralizer"::: )  "a") ->   ($#v8_struct_0 :::"finite"::: )     ($#v15_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: WEDDWITT:7 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "G")))))) ; 
 
theorem :: WEDDWITT:8 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a")))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "a")) ")" ))  ")" ))) ; 
 registrationlet "G" be   ($#l3_algstr_0 :::"Group":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); 
cluster (Set   ($#k7_group_3 :::"con_class"::: )  "a") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "a" :::"-con_map":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "("  ($#k7_group_3 :::"con_class"::: )  "a" ")" ) means :: WEDDWITT:def 2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "G" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set "a"  ($#k2_group_3 :::"|^"::: )  (Set (Var "x"))))); end; 






:: deftheorem    defines :::"-con_map"::: WEDDWITT:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set  "("  ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_group_3 :::"|^"::: )  (Set (Var "x")))))  ")" )))); 
 
theorem :: WEDDWITT:9 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "x")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_group_3 :::"con_class"::: )  (Set (Var "a"))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "a")) ")" )))))) ; 
 
theorem :: WEDDWITT:10 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set  "(" (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))))) ; 
 
theorem :: WEDDWITT:11 (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool  "{"  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) where x "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_group_3 :::"con_class"::: )  (Set (Var "a"))) : (Bool verum)  "}"   "is"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))))) ; 
 
theorem :: WEDDWITT:12 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_weddwitt :::"-con_map"::: )  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) where x "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k7_group_3 :::"con_class"::: )  (Set (Var "a"))) : (Bool verum)  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: WEDDWITT:13 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")) ")" ) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "a")) ")" ) ")" ))))) ; 
 definitionlet "G" be   ($#l3_algstr_0 :::"Group":::); func  :::"conjugate_Classes"::: "G" ->    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") equals :: WEDDWITT:def 3  "{"  (Set  "("  ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")) ")" ) where a "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool verum)  "}"  ; end; 





:: deftheorem    defines :::"conjugate_Classes"::: WEDDWITT:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#l3_algstr_0 :::"Group":::) "holds"  (Bool (Set   ($#k3_weddwitt :::"conjugate_Classes"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k7_group_3 :::"con_class"::: )  (Set (Var "a")) ")" ) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool verum)  "}"  )); 
 
theorem :: WEDDWITT:14 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_weddwitt :::"conjugate_Classes"::: )  (Set (Var "G")))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_weddwitt :::"conjugate_Classes"::: )  (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set (Var "c"))))))) ; 
 begin  
theorem :: WEDDWITT:15 (Bool  "for" (Set (Var "F")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  ) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "F")))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Skew-Field":::); func  :::"center"::: "R" ->   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Field":::) means :: WEDDWITT:def 4 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "R" : (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" "R" "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))))  "}"  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "R")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "R")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "R")) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  "R"))  ")" ); end; 





:: deftheorem    defines :::"center"::: WEDDWITT:def 4 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Field":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x")))))  "}"  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "R")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "R")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R"))))  ")" )  ")" ))); 
 
theorem :: WEDDWITT:16 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) ; 
 registrationlet "R" be   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::); 
cluster (Set   ($#k4_weddwitt :::"center"::: )  "R") ->   ($#v8_struct_0 :::"finite"::: )     ($#v36_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: WEDDWITT:17 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R")))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set (Var "y"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))))  ")" ))) ; 
 
theorem :: WEDDWITT:18 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R"))))) ; 
 
theorem :: WEDDWITT:19 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "R")))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R"))))) ; 
 
theorem :: WEDDWITT:20 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  "holds" (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))))) ; 
 
theorem :: WEDDWITT:21 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "iff" (Bool (Set (Var "R")) "is"   ($#v5_group_1 :::"commutative"::: )  )  ")" )) ; 
 
theorem :: WEDDWITT:22 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k10_group_5 :::"center"::: )  (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" ) ")" ))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Skew-Field":::); let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func  :::"centralizer"::: "s" ->   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Skew-Field":::) means :: WEDDWITT:def 5 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "R" : (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  "s")  ($#r1_hidden :::"="::: )  (Set "s"  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x"))))  "}"  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "R")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "R")  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "R")) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  "R"))  ")" ); end; 






:: deftheorem    defines :::"centralizer"::: WEDDWITT:def 5 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v36_algstr_0 :::"strict"::: )    ($#l6_algstr_0 :::"Skew-Field":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "x"))))  "}"  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "R")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3"))))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "R")))  ($#k1_realset1 :::"||"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3"))))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R"))))  ")" )  ")" )))); 
 
theorem :: WEDDWITT:23 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 
theorem :: WEDDWITT:24 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))) "iff" (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: WEDDWITT:25 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))))) ; 
 
theorem :: WEDDWITT:26 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))))) ; 
 
theorem :: WEDDWITT:27 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) & (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "R"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))  ")" ))) ; 
 registrationlet "R" be   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::); let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); 
cluster (Set   ($#k5_weddwitt :::"centralizer"::: )  "s") ->   ($#v8_struct_0 :::"finite"::: )     ($#v36_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: WEDDWITT:28 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "holds" (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )))))) ; 
 
theorem :: WEDDWITT:29 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "t")) ")" ))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; 
 
theorem :: WEDDWITT:30 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" )  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k1_weddwitt :::"Centralizer"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))))) ; 
 begin  definitionlet "R" be   ($#l6_algstr_0 :::"Skew-Field":::); func  :::"VectSp_over_center"::: "R" ->   ($#v7_vectsp_1 :::"strict"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k4_weddwitt :::"center"::: )  "R") means :: WEDDWITT:def 6 (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" it) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R") "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "R") "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" "R") "#)" )) & (Bool (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "R")  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  "R" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R") ($#k2_zfmisc_1 :::":]"::: ) )))  ")" ); end; 





:: deftheorem    defines :::"VectSp_over_center"::: WEDDWITT:def 6 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v7_vectsp_1 :::"strict"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_weddwitt :::"VectSp_over_center"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b2"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "b2"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "R"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "R"))) "#)" )) & (Bool (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "R")))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )  ")" ))); 
 
theorem :: WEDDWITT:31 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) ")" )  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k6_weddwitt :::"VectSp_over_center"::: )  (Set (Var "R")) ")" ) ")" )))) ; 
 
theorem :: WEDDWITT:32 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  "holds" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k6_weddwitt :::"VectSp_over_center"::: )  (Set (Var "R")) ")" )))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Skew-Field":::); let "s" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func  :::"VectSp_over_center"::: "s" ->   ($#v7_vectsp_1 :::"strict"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k4_weddwitt :::"center"::: )  "R") means :: WEDDWITT:def 7 (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" it) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" it) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  "s" ")" )) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  "s" ")" )) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  "s" ")" )) "#)" )) & (Bool (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" "R")  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  "R" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  "s" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" ); end; 






:: deftheorem    defines :::"VectSp_over_center"::: WEDDWITT:def 7 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v7_vectsp_1 :::"strict"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set   ($#k4_weddwitt :::"center"::: )  (Set (Var "R"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_weddwitt :::"VectSp_over_center"::: )  (Set (Var "s")))) "iff" (Bool  "("  (Bool (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "b3"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "b3"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g2_algstr_0 :::"addLoopStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) "#)" )) & (Bool (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "R")))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )  ")" )))); 
 
theorem :: WEDDWITT:33 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" )))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) ")" )  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k7_weddwitt :::"VectSp_over_center"::: )  (Set (Var "s")) ")" ) ")" ))))) ; 
 
theorem :: WEDDWITT:34 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "holds" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k7_weddwitt :::"VectSp_over_center"::: )  (Set (Var "s")) ")" ))))) ; 
 
theorem :: WEDDWITT:35 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "r")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) ")" )  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k7_weddwitt :::"VectSp_over_center"::: )  (Set (Var "r")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_int_1 :::"divides"::: )  (Set (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) ")" )  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k6_weddwitt :::"VectSp_over_center"::: )  (Set (Var "R")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))))) ; 
 
theorem :: WEDDWITT:36 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" ))) "holds"  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k7_weddwitt :::"VectSp_over_center"::: )  (Set (Var "s")) ")" ))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k6_weddwitt :::"VectSp_over_center"::: )  (Set (Var "R")) ")" ))))) ; 
 
theorem :: WEDDWITT:37 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k10_group_5 :::"center"::: )  (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "R")) ")" ) ")" )))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" )) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 begin  
theorem :: WEDDWITT:38 (Bool  "for" (Set (Var "R")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set (Var "R")) "is"   ($#v5_group_1 :::"commutative"::: )  )) ; 
 
theorem :: WEDDWITT:39 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::) "holds"  (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set  "("  ($#k4_weddwitt :::"center"::: )  (Set (Var "R")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R"))))) ; 
 
theorem :: WEDDWITT:40 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set  "("  ($#k5_weddwitt :::"centralizer"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R")))))) ;