:: HILBASIS semantic presentation begin theorem :: HILBASIS:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "fA")) "," (Set (Var "fB")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "fA")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "A")))) & (Bool (Set (Var "fB")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "fA")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "fB")))) ")" )))) ; theorem :: HILBASIS:2 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "holds" (Bool (Set ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: HILBASIS:3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "j")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "b")) ($#k5_relat_1 :::"|"::: ) (Set (Var "i"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "i")))))) ; theorem :: HILBASIS:4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "j")) (Bool "for" (Set (Var "b19")) "," (Set (Var "b29")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "i")) "st" (Bool (Bool (Set (Var "b19")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k5_relat_1 :::"|"::: ) (Set (Var "i")))) & (Bool (Set (Var "b29")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k5_relat_1 :::"|"::: ) (Set (Var "i")))) & (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "b19")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b29")))))) ; theorem :: HILBASIS:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "j")) (Bool "for" (Set (Var "b19")) "," (Set (Var "b29")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "i")) "st" (Bool (Bool (Set (Var "b19")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k5_relat_1 :::"|"::: ) (Set (Var "i")))) & (Bool (Set (Var "b29")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k5_relat_1 :::"|"::: ) (Set (Var "i"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "b1")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b2")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b19")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b29")))) & (Bool (Set (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b19")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b29")))) ")" )))) ; definitionlet "n", "k" be ($#m1_hidden :::"Nat":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); func "b" :::"bag_extend"::: "k" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) means :: HILBASIS:def 1 (Bool "(" (Bool (Set it ($#k5_relat_1 :::"|"::: ) "n") ($#r1_hidden :::"="::: ) "b") & (Bool (Set it ($#k1_recdef_1 :::"."::: ) "n") ($#r1_hidden :::"="::: ) "k") ")" ); end; :: deftheorem defines :::"bag_extend"::: HILBASIS:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_hilbasis :::"bag_extend"::: ) (Set (Var "k")))) "iff" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "b4")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" )))); theorem :: HILBASIS:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) ($#k1_hilbasis :::"bag_extend"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HILBASIS:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ))) "iff" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func :::"UnitBag"::: "x" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "X") equals :: HILBASIS:def 2 (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) "X" ")" ) ($#k2_funct_7 :::"+*"::: ) "(" "x" "," (Num 1) ")" ); end; :: deftheorem defines :::"UnitBag"::: HILBASIS:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Num 1) ")" )))); theorem :: HILBASIS:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: HILBASIS:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ))) ; theorem :: HILBASIS:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))))) ; theorem :: HILBASIS:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" ) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "e")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; func :::"1_1"::: "(" "x" "," "L" ")" -> ($#m1_subset_1 :::"Series":::) "of" "X" "," "L" equals :: HILBASIS:def 3 (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" "X" "," "L" ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) "x" ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) "L" ")" ) ")" ); end; :: deftheorem defines :::"1_1"::: HILBASIS:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ))))); theorem :: HILBASIS:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" )))) ; theorem :: HILBASIS:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_hilbasis :::"UnitBag"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; registrationlet "X" be ($#m1_hidden :::"Ordinal":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k3_hilbasis :::"1_1"::: ) "(" "x" "," "L" ")" ) -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; theorem :: HILBASIS:14 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x1")) "," (Set (Var "L")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_hilbasis :::"1_1"::: ) "(" (Set (Var "x2")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))))) ; theorem :: HILBASIS:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p"))))))) ; theorem :: HILBASIS:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "q"))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Const "L")) ")" ); func :::"minlen"::: "I" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "I" equals :: HILBASIS:def 4 "{" (Set (Var "x")) where x "is" ($#m2_subset_1 :::"Element"::: ) "of" "I" : (Bool "for" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y9")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "x9"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "y9"))))) "}" ; end; :: deftheorem defines :::"minlen"::: HILBASIS:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "holds" (Bool (Set ($#k4_hilbasis :::"minlen"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool "for" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y9")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "x9"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "y9"))))) "}" ))); theorem :: HILBASIS:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "i1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_hilbasis :::"minlen"::: ) (Set (Var "I")))) & (Bool (Set (Var "i2")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "i1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "i2")))) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"monomial"::: "(" "a" "," "n" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: HILBASIS:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "a") ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ")" )); end; :: deftheorem defines :::"monomial"::: HILBASIS:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ")" )) ")" ))))); theorem :: HILBASIS:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "implies" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "implies" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" )))) ; theorem :: HILBASIS:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: HILBASIS:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set "(" ($#k5_hilbasis :::"monomial"::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))))))) ; theorem :: HILBASIS:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))))) ; begin theorem :: HILBASIS:22 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k7_relset_1 :::".:"::: ) (Set (Var "I"))) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")))))) ; theorem :: HILBASIS:23 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_quofield :::"RingHomomorphism"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))))) ; theorem :: HILBASIS:24 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) (Bool "for" (Set (Var "lc")) "being" ($#m1_ideal_1 :::"LinearCombination"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "LC")) "being" ($#m1_ideal_1 :::"LinearCombination"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "E")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#k3_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v1_quofield :::"RingHomomorphism"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "lc"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "LC")))) & (Bool (Set (Var "E")) ($#r1_ideal_1 :::"represents"::: ) (Set (Var "lc"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "LC"))))) "holds" (Bool (Set (Set (Var "LC")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "lc")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "LC"))))))))))) ; theorem :: HILBASIS:25 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v4_quofield :::"RingIsomorphism"::: ) ))) ; theorem :: HILBASIS:26 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "F")) ($#k7_ideal_1 :::"-Ideal"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k7_relset_1 :::".:"::: ) (Set (Var "F")) ")" ) ($#k7_ideal_1 :::"-Ideal"::: ) ))))) ; theorem :: HILBASIS:27 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) ) & (Bool (Set (Var "R")) "is" ($#v6_ideal_1 :::"Noetherian"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v6_ideal_1 :::"Noetherian"::: ) ))) ; theorem :: HILBASIS:28 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "R")) ")" ")" ) "st" (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) ))) ; theorem :: HILBASIS:29 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" )) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "R")) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool (Set (Set (Var "p1")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "g")) ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ))) ")" ))))))) ; definitionlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"upm"::: "(" "n" "," "R" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "R" ")" ")" ) ")" ) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "R" ")" ")" ) means :: HILBASIS:def 6 (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "R" ")" ")" ) (Bool "for" (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "R" (Bool "for" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "R" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set "n" ($#k2_nat_1 :::"+"::: ) (Num 1)) "st" (Bool (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) "n" ")" )))) "holds" (Bool (Set (Set (Var "p3")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k5_relat_1 :::"|"::: ) "n" ")" ))))))); end; :: deftheorem defines :::"upm"::: HILBASIS:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) ")" ) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_hilbasis :::"upm"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" )) "iff" (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) (Bool "for" (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "R")) (Bool "for" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "st" (Bool (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set (Var "p3")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ))))))) ")" )))); registrationlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k6_hilbasis :::"upm"::: ) "(" "n" "," "R" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; cluster (Set ($#k6_hilbasis :::"upm"::: ) "(" "n" "," "R" ")" ) -> ($#v1_group_6 :::"multiplicative"::: ) ; cluster (Set ($#k6_hilbasis :::"upm"::: ) "(" "n" "," "R" ")" ) -> ($#v6_group_1 :::"unity-preserving"::: ) ; cluster (Set ($#k6_hilbasis :::"upm"::: ) "(" "n" "," "R" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; definitionlet "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"mpu"::: "(" "n" "," "R" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "R" ")" ")" ) "," (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "R" ")" ")" ) ")" ) means :: HILBASIS:def 7 (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "R" (Bool "for" (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "R" (Bool "for" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "R" ")" ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p3")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "p2")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_polynom1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k1_hilbasis :::"bag_extend"::: ) (Set (Var "i")) ")" )))))))); end; :: deftheorem defines :::"mpu"::: HILBASIS:def 7 : (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_hilbasis :::"mpu"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" )) "iff" (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) (Bool "for" (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "R")) (Bool "for" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "p1")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p3")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "p2")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_polynom1 :::"."::: ) (Set "(" (Set (Var "b")) ($#k1_hilbasis :::"bag_extend"::: ) (Set (Var "i")) ")" )))))))) ")" )))); theorem :: HILBASIS:30 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k6_hilbasis :::"upm"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k7_hilbasis :::"mpu"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: HILBASIS:31 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ")" ) ")" ) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "R")) ")" ")" ) "st" (Bool (Set (Var "P")) "is" ($#v4_quofield :::"RingIsomorphism"::: ) )))) ; begin registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_ideal_1 :::"Noetherian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) "R") -> ($#v6_ideal_1 :::"Noetherian"::: ) ; end; theorem :: HILBASIS:32 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v6_ideal_1 :::"Noetherian"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "R")) ")" ) "is" ($#v6_ideal_1 :::"Noetherian"::: ) ))) ; theorem :: HILBASIS:33 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Var "F")) "is" ($#v6_ideal_1 :::"Noetherian"::: ) )) ; theorem :: HILBASIS:34 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "F")) ")" ) "is" ($#v6_ideal_1 :::"Noetherian"::: ) ))) ; theorem :: HILBASIS:35 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Bool "not" (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "X")) "," (Set (Var "R")) ")" ) "is" ($#v6_ideal_1 :::"Noetherian"::: ) )))) ;