:: LOPBAN_4 semantic presentation begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); pred "x" "," "y" :::"are_commutative"::: means :: LOPBAN_4:def 1 (Bool (Set "x" ($#k6_algstr_0 :::"*"::: ) "y") ($#r1_hidden :::"="::: ) (Set "y" ($#k6_algstr_0 :::"*"::: ) "x")); reflexivity (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) ; symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))))) ; end; :: deftheorem defines :::"are_commutative"::: LOPBAN_4:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_lopban_4 :::"are_commutative"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))) ")" ))); theorem :: LOPBAN_4:1 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_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 ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq2")))))) ; theorem :: LOPBAN_4:2 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))))) ; theorem :: LOPBAN_4:3 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "s9")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k4_lopban_3 :::"*"::: ) (Set (Var "s9"))) "is" ($#v3_normsp_1 :::"convergent"::: ) ))) ; theorem :: LOPBAN_4:4 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k2_lopban_3 :::"*"::: ) (Set (Var "s"))) "is" ($#v3_normsp_1 :::"convergent"::: ) )))) ; theorem :: LOPBAN_4:5 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k3_lopban_3 :::"*"::: ) (Set (Var "z"))) "is" ($#v3_normsp_1 :::"convergent"::: ) )))) ; theorem :: LOPBAN_4:6 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "z")) ($#k2_lopban_3 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s")) ")" )))))) ; theorem :: LOPBAN_4:7 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "s")) ($#k3_lopban_3 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))))))) ; theorem :: LOPBAN_4:8 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Var "s9")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "s")) ($#k4_lopban_3 :::"*"::: ) (Set (Var "s9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s9")) ")" ))))) ; theorem :: LOPBAN_4:9 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_3 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "z")) ($#k2_lopban_3 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq")) ($#k3_lopban_3 :::"*"::: ) (Set (Var "z")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k3_lopban_3 :::"*"::: ) (Set (Var "z")))) ")" )))) ; theorem :: LOPBAN_4:10 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ")" ) ($#k8_nat_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 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: LOPBAN_4:11 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: LOPBAN_4:12 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "rseq")) ($#k8_nat_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" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" )))) ; definitionlet "X" be ($#l1_lopban_2 :::"Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "z" :::"rExpSeq"::: -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_4:def 2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "z" ($#k6_lopban_3 :::"#N"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"rExpSeq"::: LOPBAN_4:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_lopban_3 :::"#N"::: ) (Set (Var "n")) ")" )))) ")" )))); scheme :: LOPBAN_4:sch 1 ExNormSpaceCASE{ F1() -> ($#l1_lopban_2 :::"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")) ($#k8_nat_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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ))) ")" ")" )))) proof end; theorem :: LOPBAN_4:13 (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_newton :::"!"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "m")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) )) ")" ) ")" ) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Coef"::: "n" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: LOPBAN_4: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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k3_newton :::"!"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Coef"::: LOPBAN_4:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_lopban_4 :::"Coef"::: ) (Set (Var "n")))) "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 "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Coef_e"::: "n" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: LOPBAN_4: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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Coef_e"::: LOPBAN_4:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_lopban_4 :::"Coef_e"::: ) (Set (Var "n")))) "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 "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"Shift"::: "seq" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_4:def 5 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ); end; :: deftheorem defines :::"Shift"::: LOPBAN_4:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "seq")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_lopban_4 :::"Shift"::: ) (Set (Var "seq")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ) ")" ))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "X" be ($#l1_lopban_2 :::"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 :: LOPBAN_4:def 6 (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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_lopban_4 :::"Coef"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "z" ($#k6_lopban_3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "w" ($#k6_lopban_3 :::"#N"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Expan"::: LOPBAN_4:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k5_lopban_4 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_lopban_4 :::"Coef"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_lopban_3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k6_lopban_3 :::"#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")) ($#k8_nat_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_lopban_2 :::"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 :: LOPBAN_4:def 7 (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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_lopban_4 :::"Coef_e"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "z" ($#k6_lopban_3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "w" ($#k6_lopban_3 :::"#N"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Expan_e"::: LOPBAN_4:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k6_lopban_4 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_lopban_4 :::"Coef_e"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k6_lopban_3 :::"#N"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k6_lopban_3 :::"#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")) ($#k8_nat_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_lopban_2 :::"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 :: LOPBAN_4:def 8 (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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Alfa"::: LOPBAN_4:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k7_lopban_4 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); definitionlet "X" be ($#l1_lopban_2 :::"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 :: LOPBAN_4:def 9 (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 ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" "w" ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) ")" ")" )); end; :: deftheorem defines :::"Conj"::: LOPBAN_4:def 9 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k8_lopban_4 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ")" )) ")" ))))); theorem :: LOPBAN_4:14 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_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_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_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"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: LOPBAN_4:15 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (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")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )))))) ; theorem :: LOPBAN_4:16 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k4_lopban_4 :::"Shift"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )))))) ; theorem :: LOPBAN_4:17 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_3 :::"#N"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k5_lopban_4 :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: LOPBAN_4:18 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k6_lopban_4 :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k5_normsp_1 :::"*"::: ) (Set "(" ($#k5_lopban_4 :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" )))))) ; theorem :: LOPBAN_4:19 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k6_lopban_3 :::"#N"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k6_lopban_4 :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: LOPBAN_4:20 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_lopban_4 :::"rExpSeq"::: ) ) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) & (Bool (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" )) ; registrationlet "X" be ($#l1_lopban_2 :::"Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); cluster (Set "z" ($#k1_lopban_4 :::"rExpSeq"::: ) ) -> ($#v2_lopban_3 :::"norm_summable"::: ) ; end; theorem :: LOPBAN_4:21 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" ($#k5_lopban_4 :::"Expan"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" ))) ; theorem :: LOPBAN_4:22 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" ($#k7_lopban_4 :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_lopban_4 :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k6_lopban_4 :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l")) ")" )))))) ; theorem :: LOPBAN_4:23 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" ($#k7_lopban_4 :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k7_lopban_4 :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k6_lopban_4 :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )))))) ; theorem :: LOPBAN_4:24 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_lopban_4 :::"Expan_e"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: LOPBAN_4:25 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k7_lopban_4 :::"Alfa"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: LOPBAN_4:26 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_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_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k8_lopban_4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: LOPBAN_4:27 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: LOPBAN_4:28 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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_lopban_4 :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_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 :: LOPBAN_4:29 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 :: LOPBAN_4:30 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_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"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ")" )))) ; theorem :: LOPBAN_4:31 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" ($#k8_lopban_4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set "(" ($#k8_lopban_4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: LOPBAN_4:32 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" ($#k8_lopban_4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))))) ; theorem :: LOPBAN_4:33 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k8_lopban_4 :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" )))) ; definitionlet "X" be ($#l1_lopban_2 :::"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 :: LOPBAN_4:def 10 (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_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" )))); end; :: deftheorem defines :::"exp_"::: LOPBAN_4:def 10 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k9_lopban_4 :::"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_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" )))) ")" ))); definitionlet "X" be ($#l1_lopban_2 :::"Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"exp"::: "z" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: LOPBAN_4:def 11 (Set (Set "(" ($#k9_lopban_4 :::"exp_"::: ) "X" ")" ) ($#k3_funct_2 :::"."::: ) "z"); end; :: deftheorem defines :::"exp"::: LOPBAN_4:def 11 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_lopban_4 :::"exp_"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))))); theorem :: LOPBAN_4:34 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k1_lopban_4 :::"rExpSeq"::: ) ")" ))))) ; theorem :: LOPBAN_4:35 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z1")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "z2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z2")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "z2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z1"))) "," (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z2"))) ($#r1_lopban_4 :::"are_commutative"::: ) ) ")" ))) ; theorem :: LOPBAN_4:36 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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 "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z2")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z1")))))) ; theorem :: LOPBAN_4:37 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) "holds" (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X"))))) ; theorem :: LOPBAN_4:38 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" ))) ; theorem :: LOPBAN_4:39 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z"))) "is" ($#v25_algstr_0 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z")) ")" ) ($#k9_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" )) "is" ($#v25_algstr_0 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k9_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set (Var "z")))) ")" ))) ; theorem :: LOPBAN_4:40 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z"))) "," (Set (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z"))) ($#r1_lopban_4 :::"are_commutative"::: ) )))) ; theorem :: LOPBAN_4:41 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"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_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "t")) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set "(" (Set (Var "t")) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" )) "," (Set ($#k10_lopban_4 :::"exp"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_lopban_4 :::"are_commutative"::: ) ) ")" )))) ;