:: POLYNOM1 semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_struct_0 :::"degenerated"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: POLYNOM1:1 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p2"))))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1")))))) ; theorem :: POLYNOM1:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))))) ; theorem :: POLYNOM1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k6_matrlin :::"Sum"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))))) ; theorem :: POLYNOM1:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k3_pre_poly :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_matrlin :::"Sum"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "p")) ($#k3_pre_poly :::"*>"::: ) ))))) ; theorem :: POLYNOM1:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k6_matrlin :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "G")) ")" ))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); redefine func "a" :::"*"::: "p" means :: POLYNOM1:def 1 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"*"::: POLYNOM1:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "p" :::"*"::: "a" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") means :: POLYNOM1:def 2 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) "a")) ")" ) ")" ); end; :: deftheorem defines :::"*"::: POLYNOM1:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_polynom1 :::"*"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" ) ")" ) ")" ))))); theorem :: POLYNOM1:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))))) ; theorem :: POLYNOM1:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" ) ($#k1_polynom1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))))) ; theorem :: POLYNOM1:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "b")) ($#k3_pre_poly :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_pre_poly :::"*>"::: ) )))) ; theorem :: POLYNOM1:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "b")) ($#k3_pre_poly :::"*>"::: ) ) ($#k1_polynom1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_pre_poly :::"*>"::: ) )))) ; theorem :: POLYNOM1:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "q")) ")" )))))) ; theorem :: POLYNOM1:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_polynom1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_polynom1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "q")) ($#k1_polynom1 :::"*"::: ) (Set (Var "a")) ")" )))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v29_algstr_0 :::"strict"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) for ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: POLYNOM1:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYNOM1:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k1_polynom1 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))))) ; begin theorem :: POLYNOM1:14 (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 "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "S")); func :::"Support"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: POLYNOM1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "S")) ")" )); end; :: deftheorem defines :::"Support"::: POLYNOM1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S")))) ")" )) ")" ))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "S")); attr "p" is :::"finite-Support"::: means :: POLYNOM1:def 4 (Bool (Set ($#k2_polynom1 :::"Support"::: ) "p") "is" ($#v1_finset_1 :::"finite"::: ) ); end; :: deftheorem defines :::"finite-Support"::: POLYNOM1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_polynom1 :::"finite-Support"::: ) ) "iff" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )))); definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "p" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n")) ")" ) "," (Set (Const "L")); let "x" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); :: original: :::"."::: redefine func "p" :::"."::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "L"; end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode Series of "X" "," "S" is ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" ) "," "S"; end; definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); func "p" :::"+"::: "q" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L" equals :: POLYNOM1:def 5 (Set "p" ($#k1_vfunct_1 :::"+"::: ) "q"); end; :: deftheorem defines :::"+"::: POLYNOM1:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "q"))))))); theorem :: POLYNOM1:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: POLYNOM1:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "r")) ($#k3_polynom1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set (Var "r")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q"))))))) ; theorem :: POLYNOM1:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; theorem :: POLYNOM1:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "r")) ($#k3_polynom1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set (Var "r")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p"))))))) ; theorem :: POLYNOM1:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYNOM1:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "q")) ")" )))))) ; definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); :: original: :::"+"::: redefine func "p" :::"+"::: "q" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L"; commutativity (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")) "holds" (Bool (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k4_polynom1 :::"+"::: ) (Set (Var "p"))))) ; end; theorem :: POLYNOM1:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k4_polynom1 :::"+"::: ) (Set (Var "r"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k4_polynom1 :::"+"::: ) (Set (Var "r")) ")" )))))) ; definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); func "p" :::"-"::: "q" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L" equals :: POLYNOM1:def 6 (Set "p" ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) "q" ")" )); end; :: deftheorem defines :::"-"::: POLYNOM1:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "q")) ")" )))))); definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; func :::"0_"::: "(" "n" "," "S" ")" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "S" equals :: POLYNOM1:def 7 (Set (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "S" ")" )); end; :: deftheorem defines :::"0_"::: POLYNOM1:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) "holds" (Bool (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "S")) ")" ))))); theorem :: POLYNOM1:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "S")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "S"))))))) ; theorem :: POLYNOM1:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))) ; definitionlet "n" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; func :::"1_"::: "(" "n" "," "L" ")" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L" equals :: POLYNOM1:def 8 (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "L" ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) "n" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ")" ); end; :: deftheorem defines :::"1_"::: POLYNOM1:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k15_funct_7 :::"+*"::: ) "(" (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ")" )))); theorem :: POLYNOM1:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (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 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; theorem :: POLYNOM1:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); func "p" :::"*'"::: "q" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L" means :: POLYNOM1:def 9 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "n" (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "st" (Bool "(" (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "s")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s"))))) "holds" (Bool "ex" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool "(" (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_polynom1 :::"."::: ) (Set (Var "b1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "q" ($#k3_polynom1 :::"."::: ) (Set (Var "b2")) ")" ))) ")" )) ")" ) ")" ))); end; :: deftheorem defines :::"*'"::: POLYNOM1:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "s")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s"))))) "holds" (Bool "ex" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k3_polynom1 :::"."::: ) (Set (Var "b2")) ")" ))) ")" )) ")" ) ")" ))) ")" )))); theorem :: POLYNOM1:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k5_polynom1 :::"+"::: ) (Set (Var "r")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) ($#k5_polynom1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r")) ")" )))))) ; theorem :: POLYNOM1:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r")) ")" )))))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); :: original: :::"*'"::: redefine func "p" :::"*'"::: "q" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L"; commutativity (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")) "holds" (Bool (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p"))))) ; end; theorem :: POLYNOM1:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; theorem :: POLYNOM1:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))) ; theorem :: POLYNOM1:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))) ; begin registrationlet "n" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#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_polynom1 :::"finite-Support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; mode Polynomial of "n" "," "S" is ($#v1_polynom1 :::"finite-Support"::: ) ($#m1_subset_1 :::"Series":::) "of" "n" "," "S"; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "p" ($#k4_polynom1 :::"+"::: ) "q") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k5_vfunct_1 :::"-"::: ) "p") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "p" ($#k6_polynom1 :::"-"::: ) "q") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster (Set ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "S" ")" ) -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k8_polynom1 :::"1_"::: ) "(" "n" "," "L" ")" ) -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "p" ($#k9_polynom1 :::"*'"::: ) "q") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"Polynom-Ring"::: "(" "n" "," "L" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) means :: POLYNOM1:def 10 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L") ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q"))))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "L" ")" )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k8_polynom1 :::"1_"::: ) "(" "n" "," "L" ")" )) ")" ); end; :: deftheorem defines :::"Polynom-Ring"::: POLYNOM1:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3")))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q"))))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ) ")" )))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v5_group_1 :::"commutative"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; theorem :: POLYNOM1:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_polynom1 :::"1_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))) ;