:: POLYALG1 semantic presentation begin definitionlet "F" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c2" is :::"strict"::: ; struct :::"AlgebraStr"::: "over" "F" -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) "," ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "F"; aggr :::"AlgebraStr":::(# :::"carrier":::, :::"addF":::, :::"multF":::, :::"ZeroF":::, :::"OneF":::, :::"lmult"::: #) -> ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "F"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) for ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); attr "A" is :::"mix-associative"::: means :: POLYALG1:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))); end; :: deftheorem defines :::"mix-associative"::: POLYALG1:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_polyalg1 :::"mix-associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_polyalg1 :::"mix-associative"::: ) for ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; mode Algebra of "L" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_polyalg1 :::"mix-associative"::: ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L"; end; theorem :: POLYALG1:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: POLYALG1:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"Formal-Series"::: "L" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L" means :: POLYALG1:def 2 (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 :::"sequence":::) "of" "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 :::"sequence":::) "of" "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")) ($#k2_normsp_1 :::"+"::: ) (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 :::"sequence":::) "of" "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")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")))))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) "L")) ")" ); end; :: deftheorem defines :::"Formal-Series"::: POLYALG1:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_polyalg1 :::"Formal-Series"::: ) (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 "b2")))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (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")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (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")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")))))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")))) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; 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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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 ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: POLYALG1:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom3 :::"Del"::: ) "(" (Set (Var "f")) "," (Num 1) ")" )))) ; theorem :: POLYALG1:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k1_polynom3 :::"Del"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ))))) ; theorem :: POLYALG1:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v1_polyalg1 :::"strict"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; theorem :: POLYALG1:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k8_polynom3 :::"+"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_polynom3 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "q")) ")" )))))) ; theorem :: POLYALG1:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_polynom3 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYALG1:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: POLYALG1:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (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"))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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 ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v1_polyalg1 :::"strict"::: ) ; end; theorem :: POLYALG1:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#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"::: ) ; cluster (Set ($#k1_polyalg1 :::"Formal-Series"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#v2_polyalg1 :::"mix-associative"::: ) ; end; definitionlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); mode :::"Subalgebra"::: "of" "A" -> ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L" means :: POLYALG1:def 3 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A")) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "A")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "A")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "A") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "A") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" "A") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ); end; :: deftheorem defines :::"Subalgebra"::: POLYALG1:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A")))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "A")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "A")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "A"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))))) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))))) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "A"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ) ")" ))); theorem :: POLYALG1:11 (Bool "for" (Set (Var "L")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "being" ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "holds" (Bool (Set (Var "A")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "A"))))) ; theorem :: POLYALG1:12 (Bool "for" (Set (Var "L")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "C")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "C"))))) ; theorem :: POLYALG1:13 (Bool "for" (Set (Var "L")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#g1_polyalg1 :::"AlgebraStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_polyalg1 :::"AlgebraStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "B"))) "#)" )))) ; theorem :: POLYALG1:14 (Bool "for" (Set (Var "L")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "st" (Bool (Bool (Set ($#g1_polyalg1 :::"AlgebraStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "A"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_polyalg1 :::"AlgebraStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "B"))) "#)" ))) "holds" (Bool (Set (Var "A")) "is" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B"))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) for ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L"; end; registrationlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "B" be ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); cluster ($#v1_polyalg1 :::"strict"::: ) for ($#m1_polyalg1 :::"Subalgebra"::: ) "of" "B"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) for ($#m1_polyalg1 :::"Subalgebra"::: ) "of" "B"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B")); attr "A" is :::"opers_closed"::: means :: POLYALG1:def 4 (Bool "(" (Bool "A" "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "B" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "A") ")" ) & (Bool (Set ($#k5_struct_0 :::"1."::: ) "B") ($#r2_hidden :::"in"::: ) "A") & (Bool (Set ($#k4_struct_0 :::"0."::: ) "B") ($#r2_hidden :::"in"::: ) "A") ")" ); end; :: deftheorem defines :::"opers_closed"::: POLYALG1:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_polyalg1 :::"opers_closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" )))); theorem :: POLYALG1:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y9"))))))))) ; theorem :: POLYALG1:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9")))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x9")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y9"))))))))) ; theorem :: POLYALG1:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x9")))))))))) ; theorem :: POLYALG1:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "C")) "is" ($#v3_polyalg1 :::"opers_closed"::: ) ) ")" ))))) ; theorem :: POLYALG1:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_polyalg1 :::"opers_closed"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#v1_polyalg1 :::"strict"::: ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: POLYALG1:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B")))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ")" ) ")" ) ")" )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "X"))) "is" ($#v3_polyalg1 :::"opers_closed"::: ) ))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Const "L")); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B")); func :::"GenAlg"::: "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" "B" means :: POLYALG1:def 5 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" "B" "st" (Bool (Bool "A" ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) ")" ) ")" ); end; :: deftheorem defines :::"GenAlg"::: POLYALG1:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_polyalg1 :::"GenAlg"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4")))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_polyalg1 :::"Subalgebra"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) ")" ) ")" ) ")" ))))); theorem :: POLYALG1:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_polyalg1 :::"opers_closed"::: ) )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_polyalg1 :::"GenAlg"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"Polynom-Algebra"::: "L" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" "L" means :: POLYALG1:def 6 (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_polyalg1 :::"Formal-Series"::: ) "L" ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_polyalg1 :::"GenAlg"::: ) (Set (Var "A")))) ")" )); end; :: deftheorem defines :::"Polynom-Algebra"::: POLYALG1:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_polyalg1 :::"strict"::: ) ($#l1_polyalg1 :::"AlgebraStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_polyalg1 :::"Formal-Series"::: ) (Set (Var "L")) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_polyalg1 :::"GenAlg"::: ) (Set (Var "A")))) ")" )) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) "L") -> ($#v4_algstr_1 :::"Loop-like"::: ) ; end; theorem :: POLYALG1:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_polyalg1 :::"Formal-Series"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" )))) "holds" (Bool (Set (Var "A")) "is" ($#v3_polyalg1 :::"opers_closed"::: ) ))) ; theorem :: POLYALG1:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")) ")" )) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set "(" ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")) ")" )) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set "(" ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")) ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k3_polyalg1 :::"Polynom-Algebra"::: ) (Set (Var "L")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L"))))) ; theorem :: POLYALG1:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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"::: ) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k1_polyalg1 :::"Formal-Series"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L"))))) ;