:: POLYNOM7 semantic presentation begin registration cluster ($#~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"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "R")); attr "p" is :::"non-zero"::: means :: POLYNOM7:def 1 (Bool "p" ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" "X" "," "R" ")" )); end; :: deftheorem defines :::"non-zero"::: POLYNOM7:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_polynom7 :::"non-zero"::: ) ) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "R")) ")" )) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) ($#v1_polynom7 :::"non-zero"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "n") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) ($#v1_polynom1 :::"finite-Support"::: ) ($#v1_polynom7 :::"non-zero"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: POLYNOM7:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "R")) ")" )) "iff" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: POLYNOM7:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "R")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "R")) "st" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "s"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); attr "b" is :::"univariate"::: means :: POLYNOM7:def 2 (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Set ($#k13_pre_poly :::"support"::: ) "b") ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "u")) ($#k1_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"univariate"::: POLYNOM7:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b")) "is" ($#v2_polynom7 :::"univariate"::: ) ) "iff" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "u")) ($#k1_tarski :::"}"::: ) ))) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV4_VALUED_0() ($#v2_pre_poly :::"finite-support"::: ) ($#v2_polynom7 :::"univariate"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV4_VALUED_0() ($#v2_pre_poly :::"finite-support"::: ) ($#v2_polynom7 :::"univariate"::: ) -> ($#~v1_polynom2 "non" ($#v1_polynom2 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; begin theorem :: POLYNOM7:3 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: POLYNOM7:4 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" )))))) ; theorem :: POLYNOM7:5 (Bool "for" (Set (Var "L")) "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"::: ) "holds" (Bool (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) ")" ) ($#r2_quofield :::"is_ringisomorph_to"::: ) (Set (Var "L")))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "L")); attr "p" is :::"monomial-like"::: means :: POLYNOM7:def 3 (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "X" "st" (Bool "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" "X" "st" (Bool (Bool (Set (Var "b9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set "p" ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")))); end; :: deftheorem defines :::"monomial-like"::: POLYNOM7:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v3_polynom7 :::"monomial-like"::: ) ) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v3_polynom7 :::"monomial-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; mode Monomial of "X" "," "L" is ($#v3_polynom7 :::"monomial-like"::: ) ($#m1_subset_1 :::"Series":::) "of" "X" "," "L"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v3_polynom7 :::"monomial-like"::: ) -> ($#v1_polynom1 :::"finite-Support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: POLYNOM7:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) ")" ) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); func :::"Monom"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Monomial":::) "of" "X" "," "L" equals :: POLYNOM7:def 4 (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" "X" "," "L" ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" "b" "," "a" ")" ); end; :: deftheorem defines :::"Monom"::: POLYNOM7:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "m" be ($#m1_subset_1 :::"Monomial":::) "of" (Set (Const "X")) "," (Set (Const "L")); func :::"term"::: "m" -> ($#m1_hidden :::"bag":::) "of" "X" means :: POLYNOM7:def 5 (Bool "(" (Bool (Set "m" ($#k3_polynom1 :::"."::: ) it) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) "or" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) "m") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) "X")) ")" ) ")" ); end; :: deftheorem defines :::"term"::: POLYNOM7:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom7 :::"term"::: ) (Set (Var "m")))) "iff" (Bool "(" (Bool (Set (Set (Var "m")) ($#k3_polynom1 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) "or" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "m" be ($#m1_subset_1 :::"Monomial":::) "of" (Set (Const "X")) "," (Set (Const "L")); func :::"coefficient"::: "m" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: POLYNOM7:def 6 (Set "m" ($#k3_polynom1 :::"."::: ) (Set "(" ($#k2_polynom7 :::"term"::: ) "m" ")" )); end; :: deftheorem defines :::"coefficient"::: POLYNOM7:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" )))))); theorem :: POLYNOM7:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )))) ; theorem :: POLYNOM7:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) ")" )))) ; theorem :: POLYNOM7:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; theorem :: POLYNOM7:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))))))) ; theorem :: POLYNOM7:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "m")))))) ; theorem :: POLYNOM7:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "m")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "m")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: POLYNOM7:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" ")" )))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "L")); attr "p" is :::"Constant"::: means :: POLYNOM7:def 7 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "X" "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) "X"))) "holds" (Bool (Set "p" ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L"))); end; :: deftheorem defines :::"Constant"::: POLYNOM7:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_polynom7 :::"Constant"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) ")" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "X") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v4_polynom7 :::"Constant"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; mode ConstPoly of "X" "," "L" is ($#v4_polynom7 :::"Constant"::: ) ($#m1_subset_1 :::"Series":::) "of" "X" "," "L"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v4_polynom7 :::"Constant"::: ) -> ($#v3_polynom7 :::"monomial-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: POLYNOM7:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "or" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" ) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster (Set ($#k7_polynom1 :::"0_"::: ) "(" "X" "," "L" ")" ) -> ($#v4_polynom7 :::"Constant"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k8_polynom1 :::"1_"::: ) "(" "X" "," "L" ")" ) -> ($#v4_polynom7 :::"Constant"::: ) ; end; theorem :: POLYNOM7:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )))) ; theorem :: POLYNOM7:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) & (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ))) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"|"::: "(" "X" "," "L" ")" -> ($#m1_subset_1 :::"Series":::) "of" "X" "," "L" equals :: POLYNOM7:def 8 (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" "X" "," "L" ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) "X" ")" ) "," "a" ")" ); end; :: deftheorem defines :::"|"::: POLYNOM7:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) "," (Set (Var "a")) ")" ))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "a" ($#k4_polynom7 :::"|"::: ) "(" "X" "," "L" ")" ) -> ($#v4_polynom7 :::"Constant"::: ) ; end; theorem :: POLYNOM7:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))) ")" )))) ; theorem :: POLYNOM7:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" )))) ; theorem :: POLYNOM7:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )))) ; theorem :: POLYNOM7:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )))) ; theorem :: POLYNOM7:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "b")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ; theorem :: POLYNOM7:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )))) ; theorem :: POLYNOM7:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) & (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )))) ; theorem :: POLYNOM7:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "c")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "c")))))))) ; theorem :: POLYNOM7:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "p" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "L")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"*"::: "p" -> ($#m1_subset_1 :::"Series":::) "of" "X" "," "L" means :: POLYNOM7:def 9 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "X" "holds" (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "p" ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" )))); func "p" :::"*"::: "a" -> ($#m1_subset_1 :::"Series":::) "of" "X" "," "L" means :: POLYNOM7:def 10 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "X" "holds" (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) "a"))); end; :: deftheorem defines :::"*"::: POLYNOM7:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" )))) ")" )))))); :: deftheorem defines :::"*"::: POLYNOM7:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_polynom7 :::"*"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) ")" )))))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#v1_polynom1 :::"finite-Support"::: ) ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "L")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "a" ($#k5_polynom7 :::"*"::: ) "p") -> ($#v1_polynom1 :::"finite-Support"::: ) ; cluster (Set "p" ($#k6_polynom7 :::"*"::: ) "a") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM7:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k6_polynom7 :::"*"::: ) (Set (Var "a")))))))) ; theorem :: POLYNOM7:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))))))) ; theorem :: POLYNOM7:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_polynom7 :::"*"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ))))))) ; theorem :: POLYNOM7:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))))) ; theorem :: POLYNOM7:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))))) ; theorem :: POLYNOM7:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_polynom7 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))))) ; theorem :: POLYNOM7:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_polynom7 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))))) ; theorem :: POLYNOM7:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))))) ; theorem :: POLYNOM7:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k10_polynom1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a"))))))))) ;