:: POLYNOM5 semantic presentation begin theorem :: POLYNOM5:1 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYNOM5:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) ; theorem :: POLYNOM5:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYNOM5:4 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: POLYNOM5:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_hahnban1 :::"**]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; theorem :: POLYNOM5:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_hahnban1 :::"**]"::: ) ) ($#k5_algstr_0 :::"-"::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_hahnban1 :::"**]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_hahnban1 :::"[**"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k9_real_1 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k1_hahnban1 :::"**]"::: ) ))) ; theorem :: POLYNOM5:7 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "n")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_power :::"to_power"::: ) (Set (Var "n")))))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )); func :::"|.":::"p":::".|"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: POLYNOM5:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"|."::: POLYNOM5:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "p")) ($#k1_polynom5 :::".|"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ) ")" ) ")" ))); theorem :: POLYNOM5:8 (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) ")" ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: POLYNOM5:9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: POLYNOM5:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set ($#k2_polynom3 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_polynom3 :::"*>"::: ) ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom3 :::"<*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) "," (Set ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ($#k2_polynom3 :::"*>"::: ) ))) ; theorem :: POLYNOM5:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_finseq_4 :::"*>"::: ) ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) "," (Set ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) "," (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k3_finseq_4 :::"*>"::: ) ))) ; theorem :: POLYNOM5:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) "holds" (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "p")) ($#k1_polynom5 :::".|"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "q")) ($#k1_polynom5 :::".|"::: ) )))) ; theorem :: POLYNOM5:13 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "p")) ($#k1_polynom5 :::".|"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))) & (Bool (Set ($#k1_polynom5 :::"|."::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" ) ($#k1_polynom5 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "p")) ($#k1_polynom5 :::".|"::: ) ))) ")" ))) ; theorem :: POLYNOM5:14 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set ($#k1_polynom5 :::"|."::: ) (Set (Var "p")) ($#k1_polynom5 :::".|"::: ) )))) ; begin definitionlet "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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "p" :::"`^"::: "n" -> ($#m1_subset_1 :::"sequence":::) "of" "L" equals :: POLYNOM5:def 2 (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" ) ")" ) ($#k1_binop_1 :::"."::: ) "(" "p" "," "n" ")" ); end; :: deftheorem defines :::"`^"::: POLYNOM5:def 2 : (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ))))); 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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "p" ($#k2_polynom5 :::"`^"::: ) "n") -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM5:15 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_funct_2 :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:16 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Num 1)) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; theorem :: POLYNOM5:17 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Num 2)) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p")))))) ; theorem :: POLYNOM5:18 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Num 3)) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p")))))) ; theorem :: POLYNOM5: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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "p"))))))) ; theorem :: POLYNOM5: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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k2_polynom5 :::"`^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5: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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n"))) ($#r2_funct_2 :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:22 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) "," (Set (Var "n")) ")" )))))) ; theorem :: POLYNOM5:23 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (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 "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1)))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "p" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "L")); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "v" :::"*"::: "p" -> ($#m1_subset_1 :::"sequence":::) "of" "L" means :: POLYNOM5:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "v" ($#k6_algstr_0 :::"*"::: ) (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"*"::: POLYNOM5:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); registrationlet "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_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "v" ($#k3_polynom5 :::"*"::: ) "p") -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM5:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: POLYNOM5:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "v")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))))))) ; theorem :: POLYNOM5:26 (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 "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; theorem :: POLYNOM5:28 (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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "v")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:29 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "v")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "v")) ($#k3_algseq_1 :::"%>"::: ) )))) ; theorem :: POLYNOM5:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "v")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: POLYNOM5:31 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "z0", "z1" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"<%":::"z0" "," "z1":::"%>"::: -> ($#m1_subset_1 :::"sequence":::) "of" "L" equals :: POLYNOM5:def 4 (Set (Set "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) "L" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," "z0" ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Num 1) "," "z1" ")" ); end; :: deftheorem defines :::"<%"::: POLYNOM5:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z0")) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Num 1) "," (Set (Var "z1")) ")" )))); theorem :: POLYNOM5:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "z0")) ($#k3_algseq_1 :::"%>"::: ) ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "z0"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "z0")) ($#k3_algseq_1 :::"%>"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ))) ; theorem :: POLYNOM5:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z0")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "z0")) ($#k3_algseq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: POLYNOM5:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k3_algseq_1 :::"%>"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) ; theorem :: POLYNOM5:35 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "x")) ($#k3_algseq_1 :::"%>"::: ) ) ($#k11_polynom3 :::"*'"::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "y")) ($#k3_algseq_1 :::"%>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )))) ; theorem :: POLYNOM5:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "x")) ($#k3_algseq_1 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) ($#k3_algseq_1 :::"%>"::: ) ))))) ; theorem :: POLYNOM5:37 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "z0")) ($#k3_algseq_1 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "z0"))))) ; theorem :: POLYNOM5:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "z0"))) & (Bool (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "z1"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "z0", "z1" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k4_polynom5 :::"<%"::: ) "z0" "," "z1" ($#k4_polynom5 :::"%>"::: ) ) -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM5:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Num 2)))) ; theorem :: POLYNOM5:40 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Num 2)))) ; theorem :: POLYNOM5:41 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z0")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: POLYNOM5:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) ; theorem :: POLYNOM5:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "z0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "z0")) ($#k3_algseq_1 :::"%>"::: ) )))) ; theorem :: POLYNOM5:44 (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z0")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))))) ; theorem :: POLYNOM5:45 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "z0"))))) ; theorem :: POLYNOM5:46 (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) "," (Set (Var "z1")) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))))) ; theorem :: POLYNOM5:47 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "z0")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z0")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))))) ; theorem :: POLYNOM5:48 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z0")) "," (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; begin definitionlet "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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"Subst"::: "(" "p" "," "q" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: POLYNOM5:def 5 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "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" ($#m2_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" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" "q" ($#k2_polynom5 :::"`^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Subst"::: POLYNOM5:def 5 : (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_polynom5 :::"Subst"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (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" ($#m2_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")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k2_polynom5 :::"`^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )) ")" ))); theorem :: POLYNOM5:49 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set ($#k5_polynom5 :::"Subst"::: ) "(" (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) "," (Set (Var "p")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:50 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "L")) "holds" (Bool (Set ($#k5_polynom5 :::"Subst"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )))) ; theorem :: POLYNOM5:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "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 ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_polynom5 :::"Subst"::: ) "(" (Set (Var "p")) "," (Set ($#k3_algseq_1 :::"<%"::: ) (Set (Var "x")) ($#k3_algseq_1 :::"%>"::: ) ) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 1))))) ; theorem :: POLYNOM5:52 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_polynom5 :::"Subst"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 2))))) ; theorem :: POLYNOM5:53 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 "(" ($#k5_polynom5 :::"Subst"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" ) ")" ))))) ; 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")); pred "x" :::"is_a_root_of"::: "p" means :: POLYNOM5:def 6 (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" "p" "," "x" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")); end; :: deftheorem defines :::"is_a_root_of"::: POLYNOM5:def 6 : (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p"))) "iff" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" )))); 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")); attr "p" is :::"with_roots"::: means :: POLYNOM5:def 7 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) "p")); end; :: deftheorem defines :::"with_roots"::: POLYNOM5:def 7 : (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")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) ")" ))); theorem :: POLYNOM5:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))) "is" ($#v1_polynom5 :::"with_roots"::: ) )) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k9_polynom3 :::"0_."::: ) "L") -> ($#v1_polynom5 :::"with_roots"::: ) ; end; theorem :: POLYNOM5:55 (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 (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_algseq_1 :::"finite-Support"::: ) ($#v1_polynom5 :::"with_roots"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))))); end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; attr "L" is :::"algebraic-closed"::: means :: POLYNOM5:def 8 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) )); end; :: deftheorem defines :::"algebraic-closed"::: POLYNOM5:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_polynom5 :::"algebraic-closed"::: ) ) "iff" (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_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) )) ")" )); 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")); func :::"Roots"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" "L" means :: POLYNOM5:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) "p") ")" )); end; :: deftheorem defines :::"Roots"::: POLYNOM5:def 9 : (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 "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p"))) ")" )) ")" )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"NormPolynomial"::: "p" -> ($#m1_subset_1 :::"sequence":::) "of" "L" means :: POLYNOM5:def 10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))); end; :: deftheorem defines :::"NormPolynomial"::: POLYNOM5:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "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 ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (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"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#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 "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k7_polynom5 :::"NormPolynomial"::: ) "p") -> ($#v1_algseq_1 :::"finite-Support"::: ) ; end; theorem :: POLYNOM5:56 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "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 (Set "(" ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))) ; theorem :: POLYNOM5:57 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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_algseq_1 :::"len"::: ) (Set "(" ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: POLYNOM5:58 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: POLYNOM5:59 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p"))) "iff" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")))) ")" )))) ; theorem :: POLYNOM5:60 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 "(" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) ) "iff" (Bool (Set ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p"))) "is" ($#v1_polynom5 :::"with_roots"::: ) ) ")" ))) ; theorem :: POLYNOM5:61 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (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 ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom5 :::"Roots"::: ) (Set "(" ($#k7_polynom5 :::"NormPolynomial"::: ) (Set (Var "p")) ")" ))))) ; theorem :: POLYNOM5:62 (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ($#r2_cfcont_1 :::"is_continuous_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ; theorem :: POLYNOM5:63 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "x"))) ($#r2_cfcont_1 :::"is_continuous_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"FPower"::: "(" "x" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" "L" "," "L" means :: POLYNOM5:def 11 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," "n" ")" ")" )))); end; :: deftheorem defines :::"FPower"::: POLYNOM5:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "n")) ")" ")" )))) ")" ))))); theorem :: POLYNOM5:64 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) "," (Num 1) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: POLYNOM5:65 (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) "," (Num 2) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) ($#k19_valued_1 :::"(#)"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))) ; theorem :: POLYNOM5:66 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "x")))))) ; theorem :: POLYNOM5:67 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Num 1) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "x1")) ($#k25_valued_1 :::"(#)"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))) ")" ))) ; theorem :: POLYNOM5:68 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Num 2) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "x1")) ($#k25_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) ($#k19_valued_1 :::"(#)"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) ")" ))) ")" ))) ; theorem :: POLYNOM5:69 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))) ")" )))) ; theorem :: POLYNOM5:70 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set ($#k8_polynom5 :::"FPower"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "f")) ($#r2_cfcont_1 :::"is_continuous_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"Polynomial-Function"::: "(" "L" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" "L" "," "L" means :: POLYNOM5:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" "p" "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"Polynomial-Function"::: POLYNOM5:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_polynom5 :::"Polynomial-Function"::: ) "(" (Set (Var "L")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ))) ")" )))); theorem :: POLYNOM5:71 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set ($#k9_polynom5 :::"Polynomial-Function"::: ) "(" (Set ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "f")) ($#r2_cfcont_1 :::"is_continuous_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" ))) ; theorem :: POLYNOM5:72 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 2)) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (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" ($#m2_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_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "z")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k7_real_1 :::"+"::: ) (Num 1)))))) ; theorem :: POLYNOM5:73 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "z0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "z")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "z0")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ))))) ; theorem :: POLYNOM5:74 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) )) ; registration cluster (Set ($#k1_complfld :::"F_Complex"::: ) ) -> ($#v2_polynom5 :::"algebraic-closed"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#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"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_polynom5 :::"algebraic-closed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end;