:: POLYNOM2 semantic presentation begin theorem :: POLYNOM2:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "m")) ")" ")" )))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; begin theorem :: POLYNOM2:2 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))))) ; theorem :: POLYNOM2:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i9")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))))) ; theorem :: POLYNOM2: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 "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM2:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool "(" "for" (Set (Var "i9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i9")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i9")))) ")" ) ")" ))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYNOM2:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool "(" "for" (Set (Var "i9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i9")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i9")))) ")" ) ")" ))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYNOM2:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: POLYNOM2:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ))) & (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j"))))))) ; theorem :: POLYNOM2:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ))) & (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k5_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))))))))) ; theorem :: POLYNOM2:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ))) & (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))))))))) ; theorem :: POLYNOM2:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ))) & (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "k")) "," (Set (Var "a")) ")" )))))))) ; begin theorem :: POLYNOM2:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); attr "b" is :::"empty"::: means :: POLYNOM2:def 1 (Bool "b" ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) "X")); end; :: deftheorem defines :::"empty"::: POLYNOM2:def 1 : (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" ($#v1_polynom2 :::"empty"::: ) ) "iff" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) ")" ))); 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"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() bbbadV4_VALUED_0() ($#v2_pre_poly :::"finite-support"::: ) ($#~v1_polynom2 "non" ($#v1_polynom2 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); :: original: :::"support"::: redefine func :::"support"::: "b" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: POLYNOM2:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n"))) ($#r3_orders_1 :::"linearly_orders"::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "X")); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); :: original: :::"*"::: redefine func "b" :::"*"::: "x" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"eval"::: "(" "b" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: POLYNOM2:def 2 (Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) "n" ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) "b" ")" ) ")" ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" "x" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) "n" ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) "b" ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" "b" ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) "n" ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) "b" ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"eval"::: POLYNOM2:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (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 "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" ")" ))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" (Set (Var "b")) ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" )) ")" )))))); theorem :: POLYNOM2:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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 "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))))) ; theorem :: POLYNOM2:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (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 "u")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "u")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set (Var "u")) ")" ) ")" ))))))) ; theorem :: POLYNOM2:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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 "b1")) "," (Set (Var "b2")) "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 ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b1")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b2")) "," (Set (Var "x")) ")" ")" ))))))) ; begin registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "p" ($#k6_polynom1 :::"-"::: ) "q") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM2:17 (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 "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); 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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k2_polynom1 :::"Support"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: POLYNOM2:18 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n"))) ($#r3_orders_1 :::"linearly_orders"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))))))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n"))); func "b" :::"@"::: -> ($#m1_hidden :::"bag":::) "of" "n" equals :: POLYNOM2:def 3 "b"; end; :: deftheorem defines :::"@"::: POLYNOM2:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b")) ($#k4_polynom2 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b"))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); 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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"eval"::: "(" "p" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: POLYNOM2:def 4 (Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) "n" ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) ")" ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "p" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) "n" ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) "n" ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k4_polynom2 :::"@"::: ) ")" ) "," "x" ")" ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"eval"::: POLYNOM2:def 4 : (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ")" ))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k4_polynom2 :::"@"::: ) ")" ) "," (Set (Var "x")) ")" ")" ))) ")" ) ")" )) ")" )))))); theorem :: POLYNOM2:19 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) "holds" (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 "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k3_polynom2 :::"eval"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" ")" )))))))) ; theorem :: POLYNOM2:20 (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 "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; theorem :: POLYNOM2:21 (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 "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set "(" ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))))) ; theorem :: POLYNOM2:22 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "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 "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: POLYNOM2:23 (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"::: ) ($#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 "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 "(" (Set (Var "p")) ($#k5_polynom1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: POLYNOM2: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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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 "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 "(" (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" ))))))) ; theorem :: POLYNOM2:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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 "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 "(" (Set (Var "p")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" ))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); 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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"Polynom-Evaluation"::: "(" "n" "," "L" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" ) "," "L" means :: POLYNOM2:def 5 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," "x" ")" ))); end; :: deftheorem defines :::"Polynom-Evaluation"::: POLYNOM2:def 5 : (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 "x")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom2 :::"Polynom-Evaluation"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_polynom2 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ))) ")" ))))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#v4_vectsp_1 :::"well-unital"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k6_polynom2 :::"Polynom-Evaluation"::: ) "(" "n" "," "L" "," "x" ")" ) -> ($#v6_group_1 :::"unity-preserving"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" 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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k6_polynom2 :::"Polynom-Evaluation"::: ) "(" "n" "," "L" "," "x" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k6_polynom2 :::"Polynom-Evaluation"::: ) "(" "n" "," "L" "," "x" ")" ) -> ($#v1_group_6 :::"multiplicative"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k6_polynom2 :::"Polynom-Evaluation"::: ) "(" "n" "," "L" "," "x" ")" ) -> ($#v1_quofield :::"RingHomomorphism"::: ) ; end;