:: CLOPBAN4 semantic presentation begin theorem :: CLOPBAN4:1 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "seq2")))))) ; theorem :: CLOPBAN4:2 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) "holds" (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))))) ; theorem :: CLOPBAN4:3 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "s")) "," (Set (Var "s9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set (Var "s9")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k4_clopban3 :::"*"::: ) (Set (Var "s9"))) "is" ($#v9_clvect_1 :::"convergent"::: ) ))) ; theorem :: CLOPBAN4:4 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k2_clopban3 :::"*"::: ) (Set (Var "s"))) "is" ($#v9_clvect_1 :::"convergent"::: ) )))) ; theorem :: CLOPBAN4:5 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k3_clopban3 :::"*"::: ) (Set (Var "z"))) "is" ($#v9_clvect_1 :::"convergent"::: ) )))) ; theorem :: CLOPBAN4:6 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set "(" (Set (Var "z")) ($#k2_clopban3 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clvect_1 :::"lim"::: ) (Set (Var "s")) ")" )))))) ; theorem :: CLOPBAN4:7 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set "(" (Set (Var "s")) ($#k3_clopban3 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_clvect_1 :::"lim"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))))) ; theorem :: CLOPBAN4:8 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "s")) "," (Set (Var "s9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set (Var "s9")) "is" ($#v9_clvect_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set "(" (Set (Var "s")) ($#k4_clopban3 :::"*"::: ) (Set (Var "s9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_clvect_1 :::"lim"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clvect_1 :::"lim"::: ) (Set (Var "s9")) ")" ))))) ; theorem :: CLOPBAN4:9 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k2_clopban3 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "z")) ($#k2_clopban3 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq")) ($#k3_clopban3 :::"*"::: ) (Set (Var "z")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k3_clopban3 :::"*"::: ) (Set (Var "z")))) ")" )))) ; theorem :: CLOPBAN4:10 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: CLOPBAN4:11 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: CLOPBAN4:12 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" )))) ; definitionlet "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "z" :::"ExpSeq"::: -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLOPBAN4:def 1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" "z" ($#k6_clopban3 :::"#N"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"ExpSeq"::: CLOPBAN4:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_clopban3 :::"#N"::: ) (Set (Var "n")) ")" )))) ")" )))); scheme :: CLOPBAN4:sch 1 ExNormSpaceCASE{ F1() -> ($#l1_clopban2 :::"Complex_Banach_Algebra":::), F2( ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) -> ($#m1_subset_1 :::"Point":::) "of" (Set F1 "(" ")" ) } : (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "k")) "," (Set (Var "n")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ))) ")" ")" )))) proof end; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"Expan"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLOPBAN4:def 2 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_sin_cos :::"Coef"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" "z" ($#k6_clopban3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "w" ($#k6_clopban3 :::"#N"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Expan"::: CLOPBAN4:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_clopban4 :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_sin_cos :::"Coef"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_clopban3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k6_clopban3 :::"#N"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"Expan_e"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLOPBAN4:def 3 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos :::"Coef_e"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" "z" ($#k6_clopban3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "w" ($#k6_clopban3 :::"#N"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Expan_e"::: CLOPBAN4:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos :::"Coef_e"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_clopban3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k6_clopban3 :::"#N"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"Alfa"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLOPBAN4:def 4 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Alfa"::: CLOPBAN4:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_clopban4 :::"Alfa"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); definitionlet "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Conj"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLOPBAN4:def 5 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) "n" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Conj"::: CLOPBAN4:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); theorem :: CLOPBAN4:13 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: CLOPBAN4:14 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k4_lopban_4 :::"Shift"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )))))) ; theorem :: CLOPBAN4:15 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k4_lopban_4 :::"Shift"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" )))))) ; theorem :: CLOPBAN4:16 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "w")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k6_clopban3 :::"#N"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k2_clopban4 :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLOPBAN4:17 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k6_clvect_1 :::"*"::: ) (Set "(" ($#k2_clopban4 :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" )))))) ; theorem :: CLOPBAN4:18 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "w")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool (Set (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k6_clopban3 :::"#N"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLOPBAN4:19 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_clopban4 :::"ExpSeq"::: ) ) "is" ($#v2_clopban3 :::"norm_summable"::: ) ) & (Bool (Set ($#k1_clopban3 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_clopban4 :::"ExpSeq"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" )) ; registrationlet "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); cluster (Set "z" ($#k1_clopban4 :::"ExpSeq"::: ) ) -> ($#v2_clopban3 :::"norm_summable"::: ) ; end; theorem :: CLOPBAN4:20 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" ($#k2_clopban4 :::"Expan"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" ))) ; theorem :: CLOPBAN4:21 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k4_clopban4 :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_clopban4 :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "l")) ")" )))))) ; theorem :: CLOPBAN4:22 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k4_clopban4 :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k4_clopban4 :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" )))))) ; theorem :: CLOPBAN4:23 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_clopban4 :::"Expan_e"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: CLOPBAN4:24 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "w")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k4_clopban4 :::"Alfa"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLOPBAN4:25 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z")) "," (Set (Var "w")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: CLOPBAN4:26 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLOPBAN4:27 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ))) ")" )))) ; theorem :: CLOPBAN4:28 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ))))) ; theorem :: CLOPBAN4:29 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "implies" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ")" )))) ; theorem :: CLOPBAN4:30 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLOPBAN4:31 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))))) ; theorem :: CLOPBAN4:32 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k5_clopban4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v9_clvect_1 :::"convergent"::: ) ) & (Bool (Set ($#k7_clvect_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" )))) ; definitionlet "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); func :::"exp_"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") means :: CLOPBAN4:def 6 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clopban3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" )))); end; :: deftheorem defines :::"exp_"::: CLOPBAN4:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_clopban4 :::"exp_"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clopban3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" )))) ")" ))); definitionlet "X" be ($#l1_clopban2 :::"Complex_Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"exp"::: "z" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: CLOPBAN4:def 7 (Set (Set "(" ($#k6_clopban4 :::"exp_"::: ) "X" ")" ) ($#k3_funct_2 :::"."::: ) "z"); end; :: deftheorem defines :::"exp"::: CLOPBAN4:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_clopban4 :::"exp_"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))))); theorem :: CLOPBAN4:33 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clopban3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_clopban4 :::"ExpSeq"::: ) ")" ))))) ; theorem :: CLOPBAN4:34 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z1")) "," (Set (Var "z2")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool "(" (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "z2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z2")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "z2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z1"))) "," (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z2"))) ($#r1_lopban_4 :::"are_commutative"::: ) ) ")" ))) ; theorem :: CLOPBAN4:35 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "z1")) "," (Set (Var "z2")) ($#r1_lopban_4 :::"are_commutative"::: ) )) "holds" (Bool (Set (Set (Var "z1")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z2")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z1")))))) ; theorem :: CLOPBAN4:36 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) "holds" (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X"))))) ; theorem :: CLOPBAN4:37 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" ))) ; theorem :: CLOPBAN4:38 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z"))) "is" ($#v25_algstr_0 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set (Var "z")) ")" ) ($#k9_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" )) "is" ($#v25_algstr_0 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k9_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set (Var "z")))) ")" ))) ; theorem :: CLOPBAN4:39 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z"))) "," (Set (Set (Var "t")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z"))) ($#r1_lopban_4 :::"are_commutative"::: ) )))) ; theorem :: CLOPBAN4:40 (Bool "for" (Set (Var "X")) "being" ($#l1_clopban2 :::"Complex_Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "t")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "t")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" )) "," (Set ($#k7_clopban4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_clvect_1 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_lopban_4 :::"are_commutative"::: ) ) ")" )))) ;