:: POLYNOM4 semantic presentation begin theorem :: POLYNOM4:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "p")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; begin theorem :: POLYNOM4:2 (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 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM4:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYNOM4:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: POLYNOM4:5 (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 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM4:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "q")) ")" )))))) ; theorem :: POLYNOM4:7 (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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" )))) ; theorem :: POLYNOM4:8 (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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: POLYNOM4:9 (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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "q")) ")" )))))) ; theorem :: POLYNOM4:10 (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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"Leading-Monomial"::: "p" -> ($#m1_subset_1 :::"sequence":::) "of" "L" means :: POLYNOM4:def 1 (Bool "(" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)))) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ) ")" ); end; :: deftheorem defines :::"Leading-Monomial"::: POLYNOM4:def 1 : (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 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ) ")" )))); theorem :: POLYNOM4:11 (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 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" )))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) "p") -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM4:12 (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 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM4:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) ; theorem :: POLYNOM4:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L"))))) ; theorem :: POLYNOM4:15 (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 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: POLYNOM4:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "q")) ($#k2_normsp_1 :::"+"::: ) (Set "(" ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "q")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"eval"::: "(" "p" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: POLYNOM4:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k2_binop_1 :::"."::: ) "(" "x" "," (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"eval"::: POLYNOM4:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" ))) ")" ) ")" )) ")" )))); theorem :: POLYNOM4:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM4:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM4:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k8_polynom3 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: POLYNOM4:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: POLYNOM4:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: POLYNOM4:22 (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_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ")" )))))) ; theorem :: POLYNOM4:23 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set "(" ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k1_polynom4 :::"Leading-Monomial"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: POLYNOM4:24 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"Polynom-Evaluation"::: "(" "L" "," "x" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" ) "," "L" means :: POLYNOM4:def 3 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," "x" ")" ))); end; :: deftheorem defines :::"Polynom-Evaluation"::: POLYNOM4:def 3 : (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_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom4 :::"Polynom-Evaluation"::: ) "(" (Set (Var "L")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ))) ")" )))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k3_polynom4 :::"Polynom-Evaluation"::: ) "(" "L" "," "x" ")" ) -> ($#v6_group_1 :::"unity-preserving"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k3_polynom4 :::"Polynom-Evaluation"::: ) "(" "L" "," "x" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; end; registrationlet "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k3_polynom4 :::"Polynom-Evaluation"::: ) "(" "L" "," "x" ")" ) -> ($#v1_group_6 :::"multiplicative"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k3_polynom4 :::"Polynom-Evaluation"::: ) "(" "L" "," "x" ")" ) -> ($#v1_quofield :::"RingHomomorphism"::: ) ; end;