:: BINOM semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 :: BINOM:1 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; theorem :: BINOM:2 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; begin theorem :: BINOM:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: BINOM:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "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 :: BINOM:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "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"))))))) ; theorem :: BINOM:6 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool (Set (Set (Var "p")) ($#k1_polynom1 :::"*"::: ) (Set (Var "a"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p", "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); func "p" :::"+"::: "q" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") means :: BINOM:def 1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "q" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"+"::: BINOM:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_binom :::"+"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); theorem :: BINOM:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k1_binom :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "q")) ")" ))))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); let "n" be ($#m1_hidden :::"Nat":::); func "a" :::"|^"::: "n" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: BINOM:def 2 (Set (Set "(" ($#k4_group_1 :::"power"::: ) "R" ")" ) ($#k1_binop_1 :::"."::: ) "(" "a" "," "n" ")" ); end; :: deftheorem defines :::"|^"::: BINOM:def 2 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "R")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ))))); theorem :: BINOM:8 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: BINOM:9 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BINOM:10 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "m")) ")" )))))) ; theorem :: BINOM:11 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_binom :::"|^"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m")) ")" )))))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"Nat-mult-left"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") means :: BINOM:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "n")) "," (Set (Var "a")) ")" ")" ))) ")" ) ")" )); func :::"Nat-mult-right"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") means :: BINOM:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "R")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a")))) ")" ) ")" )); end; :: deftheorem defines :::"Nat-mult-left"::: BINOM:def 3 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "n")) "," (Set (Var "a")) ")" ")" ))) ")" ) ")" )) ")" ))); :: deftheorem defines :::"Nat-mult-right"::: BINOM:def 4 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_binom :::"Nat-mult-right"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a")))) ")" ) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"*"::: "a" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: BINOM:def 5 (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) "R" ")" ) ($#k2_binop_1 :::"."::: ) "(" "n" "," "a" ")" ); func "a" :::"*"::: "n" -> ($#m1_subset_1 :::"Element":::) "of" "R" equals :: BINOM:def 6 (Set (Set "(" ($#k4_binom :::"Nat-mult-right"::: ) "R" ")" ) ($#k2_binop_1 :::"."::: ) "(" "a" "," "n" ")" ); end; :: deftheorem defines :::"*"::: BINOM:def 5 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "n")) "," (Set (Var "a")) ")" ))))); :: deftheorem defines :::"*"::: BINOM:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_binom :::"Nat-mult-right"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ))))); theorem :: BINOM:12 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) & (Bool (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ))) ; theorem :: BINOM:13 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Num 1) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: BINOM:14 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: BINOM:15 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "m")) ($#k5_binom :::"*"::: ) (Set (Var "a")) ")" )))))) ; theorem :: BINOM:16 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "m")) ")" )))))) ; theorem :: BINOM:17 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "n"))))))) ; theorem :: BINOM:18 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "n"))))))) ; theorem :: BINOM:19 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: BINOM:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_binom :::"*"::: ) (Set (Var "n"))))))) ; theorem :: BINOM:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_binom :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k5_binom :::"*"::: ) (Set (Var "b")) ")" )))))) ; begin definitionlet "k", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"choose"::: redefine func "n" :::"choose"::: "k" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "(" "a" "," "b" ")" :::"In_Power"::: "n" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") means :: BINOM:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set "n" ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it)) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set "n" ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m"))))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "n" ($#k7_binom :::"choose"::: ) (Set (Var "m")) ")" ) ($#k5_binom :::"*"::: ) (Set "(" "a" ($#k2_binom :::"|^"::: ) (Set (Var "l")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "b" ($#k2_binom :::"|^"::: ) (Set (Var "m")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"In_Power"::: BINOM:def 7 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k8_binom :::"In_Power"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k7_binom :::"choose"::: ) (Set (Var "m")) ")" ) ($#k5_binom :::"*"::: ) (Set "(" (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "l")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Set (Var "m")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: BINOM:22 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#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 "R")) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k8_binom :::"In_Power"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: BINOM:23 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k8_binom :::"In_Power"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: BINOM:24 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k8_binom :::"In_Power"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_binom :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: BINOM:25 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_binom :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k8_binom :::"In_Power"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BINOM:26 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "n")) "," (Set (Var "a")) ")" ")" ) ")" )) ")" ) ")" )))))) ; theorem :: BINOM:27 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "a")) ")" )) ")" ) ")" )))))) ;