:: SEQ_4 semantic presentation begin theorem :: SEQ_4:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) ")" )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) ")" )))) ; theorem :: SEQ_4:2 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "r")) ($#k9_binop_2 :::"+"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "holds" (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; theorem :: SEQ_4:3 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))))) ; theorem :: SEQ_4:4 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" ) ")" )) ")" )) ; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"{"::: redefine func :::"{":::"r":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: SEQ_4:5 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "g")) ($#k10_binop_2 :::"-"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" ) ")" ))) ; theorem :: SEQ_4:6 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g1"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "g1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g2"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "g2")) ($#k10_binop_2 :::"-"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" )) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))))) ; theorem :: SEQ_4:7 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g")) ($#k9_binop_2 :::"+"::: ) (Set (Var "s")))) ")" )) ")" ) ")" ))) ; theorem :: SEQ_4:8 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "g1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "s")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "g2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g2")) ($#k9_binop_2 :::"+"::: ) (Set (Var "s")))) ")" )) ")" )) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))))) ; definitionlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; assume (Bool "(" (Bool (Bool "not" (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Const "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ) ; func :::"upper_bound"::: "X" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) means :: SEQ_4:def 1 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set it ($#k10_binop_2 :::"-"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"upper_bound"::: SEQ_4:def 1 : (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "b2")) ($#k10_binop_2 :::"-"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" ) ")" ) ")" ))); definitionlet "X" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; assume (Bool "(" (Bool (Bool "not" (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Const "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" ) ; func :::"lower_bound"::: "X" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) means :: SEQ_4:def 2 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set it ($#k9_binop_2 :::"+"::: ) (Set (Var "s")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"lower_bound"::: SEQ_4:def 2 : (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "b2")) ($#k9_binop_2 :::"+"::: ) (Set (Var "s")))) ")" )) ")" ) ")" ) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) ($#m1_hidden :::"set"::: ) ; identify ; end; definitionlet "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"upper_bound"::: redefine func :::"upper_bound"::: "X" -> ($#m1_subset_1 :::"Real":::); :: original: :::"lower_bound"::: redefine func :::"lower_bound"::: "X" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SEQ_4:9 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) ; theorem :: SEQ_4:10 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: SEQ_4:11 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X"))))) ; theorem :: SEQ_4:12 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool "ex" (Set (Var "r")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "r"))) ")" )) "iff" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")))) ")" )) ; theorem :: SEQ_4:13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) ; registrationlet "seq" be ($#v2_comseq_2 :::"convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::); cluster (Set ($#k54_valued_1 :::"|."::: ) "seq" ($#k54_valued_1 :::".|"::: ) ) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Real_Sequence":::); end; theorem :: SEQ_4:14 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")) ")" )))) ; theorem :: SEQ_4:15 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: SEQ_4:16 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) ; theorem :: SEQ_4:17 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))))) ; theorem :: SEQ_4:18 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) ; theorem :: SEQ_4:19 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1"))))) ; registration cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "seq" be ($#v2_comseq_2 :::"convergent"::: ) ($#m1_subset_1 :::"Real_Sequence":::); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "seq" ($#k9_nat_1 :::"^\"::: ) "k") -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Real_Sequence":::); end; theorem :: SEQ_4:20 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: SEQ_4:21 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ))) ; theorem :: SEQ_4:22 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQ_4:23 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_relat_1 :::"non-zero"::: ) ))) ; theorem :: SEQ_4:24 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq1")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) ")" ))) ; theorem :: SEQ_4:25 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "seq")))) "or" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ")" )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))))) ; theorem :: SEQ_4:26 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SEQ_4:27 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq1")) "is" ($#v2_relat_1 :::"non-zero"::: ) )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k37_valued_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k8_binop_2 :::"""::: ) )))) ; theorem :: SEQ_4:28 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ))) ; theorem :: SEQ_4:29 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SEQ_4:30 (Bool "for" (Set (Var "seq")) "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 (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k18_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: SEQ_4:31 (Bool "for" (Set (Var "r")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: SEQ_4:32 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ))) ; theorem :: SEQ_4:33 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SEQ_4:34 (Bool "for" (Set (Var "seq")) "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 (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k18_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: SEQ_4:35 (Bool "for" (Set (Var "r")) "," (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; registration cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) bbbadV7_VALUED_0() ($#v1_seq_2 :::"bounded_above"::: ) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) bbbadV8_VALUED_0() ($#v2_seq_2 :::"bounded_below"::: ) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_seqm_3 :::"monotone"::: ) ($#v1_comseq_2 :::"bounded"::: ) -> ($#v2_comseq_2 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: SEQ_4:36 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seqm_3 :::"monotone"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) ; theorem :: SEQ_4:37 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "seq")) "is" bbbadV7_VALUED_0())) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: SEQ_4:38 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "seq")) "is" bbbadV8_VALUED_0())) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SEQ_4:39 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "ex" (Set (Var "Nseq")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Nseq"))) "is" ($#v1_seqm_3 :::"monotone"::: ) ))) ; theorem :: SEQ_4:40 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool "ex" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ))) ; theorem :: SEQ_4:41 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "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 ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))))) ")" )) ; theorem :: SEQ_4:42 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1")) ")" ))) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1")) ")" ))) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq1")) ")" ))) ")" )) ; begin theorem :: SEQ_4:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t"))))) ; theorem :: SEQ_4:44 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "X")))))) ; theorem :: SEQ_4:45 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))))) ; theorem :: SEQ_4:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) ")" )) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "X")))))) ; theorem :: SEQ_4:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "Y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set (Var "X")))))) ; theorem :: SEQ_4:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set (Var "Y")))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; :: original: :::"inf"::: redefine func :::"min"::: "A" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; begin theorem :: SEQ_4:49 (Bool (Set ($#k5_complex1 :::"0c"::: ) ) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) ; theorem :: SEQ_4:50 (Bool (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) ; theorem :: SEQ_4:51 (Bool (Set ($#k27_binop_2 :::"addcomplex"::: ) ) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) ; theorem :: SEQ_4:52 (Bool (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) ($#r2_funct_2 :::"="::: ) (Set ($#k25_binop_2 :::"compcomplex"::: ) )) ; definitionredefine func :::"diffcomplex"::: equals :: SEQ_4:def 3 (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "," (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ")" ); end; :: deftheorem defines :::"diffcomplex"::: SEQ_4:def 3 : (Bool (Set ($#k28_binop_2 :::"diffcomplex"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "," (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ")" )); theorem :: SEQ_4:53 (Bool (Set ($#k6_complex1 :::"1r"::: ) ) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k29_binop_2 :::"multcomplex"::: ) )) ; theorem :: SEQ_4:54 (Bool (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) ; definitionlet "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "c" :::"multcomplex"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 4 (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k5_funcop_1 :::"[;]"::: ) "(" "c" "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"multcomplex"::: SEQ_4:def 4 : (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k7_seq_4 :::"multcomplex"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "c")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) ")" ))); theorem :: SEQ_4:55 (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k7_seq_4 :::"multcomplex"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c9"))))) ; theorem :: SEQ_4:56 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "c")) ($#k7_seq_4 :::"multcomplex"::: ) ) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) ))) ; definitionfunc :::"abscomplex"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQ_4:def 5 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c")) ($#k17_complex1 :::".|"::: ) ))); end; :: deftheorem defines :::"abscomplex"::: SEQ_4:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_seq_4 :::"abscomplex"::: ) )) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c")) ($#k17_complex1 :::".|"::: ) ))) ")" )); definitionlet "z1", "z2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"+"::: redefine func "z1" :::"+"::: "z2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 6 (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" "z1" "," "z2" ")" ); :: original: :::"-"::: redefine func "z1" :::"-"::: "z2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 7 (Set (Set ($#k28_binop_2 :::"diffcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" "z1" "," "z2" ")" ); end; :: deftheorem defines :::"+"::: SEQ_4:def 6 : (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "z1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ))); :: deftheorem defines :::"-"::: SEQ_4:def 7 : (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "z1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k28_binop_2 :::"diffcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ))); definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"-"::: redefine func :::"-"::: "z" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 8 (Set (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ($#k4_finseqop :::"*"::: ) "z"); end; :: deftheorem defines :::"-"::: SEQ_4:def 8 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k11_seq_4 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ($#k4_finseqop :::"*"::: ) (Set (Var "z"))))); notationlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; synonym "c" :::"*"::: "z" for "c" :::"(#)"::: "z"; end; definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*"::: redefine func "c" :::"*"::: "z" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 9 (Set (Set "(" "c" ($#k7_seq_4 :::"multcomplex"::: ) ")" ) ($#k4_finseqop :::"*"::: ) "z"); end; :: deftheorem defines :::"*"::: SEQ_4:def 9 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k7_seq_4 :::"multcomplex"::: ) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "z")))))); definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"|."::: redefine func :::"abs"::: "z" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SEQ_4:def 10 (Set (Set ($#k8_seq_4 :::"abscomplex"::: ) ) ($#k4_finseqop :::"*"::: ) "z"); end; :: deftheorem defines :::"abs"::: SEQ_4:def 10 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k13_seq_4 :::"abs"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_seq_4 :::"abscomplex"::: ) ) ($#k4_finseqop :::"*"::: ) (Set (Var "z"))))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"COMPLEX"::: "n" -> ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 11 (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); end; :: deftheorem defines :::"COMPLEX"::: SEQ_4:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))); registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: SEQ_4:57 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z1", "z2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); :: original: :::"+"::: redefine func "z1" :::"+"::: "z2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n"); end; theorem :: SEQ_4:58 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Var "c2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2"))))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"0c"::: "n" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SEQ_4:def 12 (Set "n" ($#k5_finseq_2 :::"|->"::: ) (Set ($#k5_complex1 :::"0c"::: ) )); end; :: deftheorem defines :::"0c"::: SEQ_4:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k16_seq_4 :::"0c"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k5_complex1 :::"0c"::: ) )))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"0c"::: redefine func :::"0c"::: "n" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n"); end; theorem :: SEQ_4:59 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k15_seq_4 :::"+"::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z")))) ")" ))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); :: original: :::"-"::: redefine func :::"-"::: "z" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n"); end; theorem :: SEQ_4:60 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "c"))))))) ; theorem :: SEQ_4:61 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k15_seq_4 :::"+"::: ) (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")))) ")" ))) ; theorem :: SEQ_4:62 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z2")))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z1")))) ")" ))) ; theorem :: SEQ_4:63 canceled; theorem :: SEQ_4:64 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z2"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))))) ; theorem :: SEQ_4:65 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool "(" (Bool (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z")))) "or" (Bool (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")))) ")" )) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))))) ; theorem :: SEQ_4:66 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k18_seq_4 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z1", "z2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); :: original: :::"-"::: redefine func "z1" :::"-"::: "z2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n"); end; theorem :: SEQ_4:67 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))))) ; theorem :: SEQ_4:68 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z")) ($#k19_seq_4 :::"-"::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: SEQ_4:69 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" ) ($#k19_seq_4 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z")))))) ; theorem :: SEQ_4:70 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")))))) ; theorem :: SEQ_4:71 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k18_seq_4 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z1")))))) ; theorem :: SEQ_4:72 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k18_seq_4 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")))))) ; theorem :: SEQ_4:73 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")))))) ; theorem :: SEQ_4:74 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))))) ; theorem :: SEQ_4:75 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k19_seq_4 :::"-"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z3")) ")" ))))) ; theorem :: SEQ_4:76 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k19_seq_4 :::"-"::: ) (Set (Var "z3")))))) ; theorem :: SEQ_4:77 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z3")))))) ; theorem :: SEQ_4:78 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z3")) ")" ) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")))))) ; theorem :: SEQ_4:79 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z")) ")" ) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")))))) ; theorem :: SEQ_4:80 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z2"))))) ; theorem :: SEQ_4:81 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set (Var "z")))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"*"::: redefine func "c" :::"*"::: "z" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n"); end; theorem :: SEQ_4:82 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c9")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c9"))))))) ; theorem :: SEQ_4:83 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "c1")) ($#k20_seq_4 :::"*"::: ) (Set "(" (Set (Var "c2")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c2")) ")" ) ($#k20_seq_4 :::"*"::: ) (Set (Var "z"))))))) ; theorem :: SEQ_4:84 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2")) ")" ) ($#k20_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c1")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" )))))) ; theorem :: SEQ_4:85 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z1")) ")" ) ($#k15_seq_4 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z2")) ")" )))))) ; theorem :: SEQ_4:86 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k6_complex1 :::"1r"::: ) ) ($#k20_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: SEQ_4:87 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k5_complex1 :::"0c"::: ) ) ($#k20_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")))))) ; theorem :: SEQ_4:88 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" ($#k1_binop_2 :::"-"::: ) (Set ($#k6_complex1 :::"1r"::: ) ) ")" ) ($#k20_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k18_seq_4 :::"-"::: ) (Set (Var "z")))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); :: original: :::"|."::: redefine func :::"abs"::: "z" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: SEQ_4:89 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" ($#k21_seq_4 :::"abs"::: ) (Set (Var "z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c")) ($#k17_complex1 :::".|"::: ) ))))) ; theorem :: SEQ_4:90 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k21_seq_4 :::"abs"::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SEQ_4:91 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k21_seq_4 :::"abs"::: ) (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k21_seq_4 :::"abs"::: ) (Set (Var "z")))))) ; theorem :: SEQ_4:92 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k21_seq_4 :::"abs"::: ) (Set "(" (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c")) ($#k17_complex1 :::".|"::: ) ) ($#k11_rvsum_1 :::"*"::: ) (Set "(" ($#k21_seq_4 :::"abs"::: ) (Set (Var "z")) ")" )))))) ; definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"|.":::"z":::".|"::: -> ($#m1_subset_1 :::"Real":::) equals :: SEQ_4:def 13 (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" ($#k13_seq_4 :::"abs"::: ) "z" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"|."::: SEQ_4:def 13 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" ($#k13_seq_4 :::"abs"::: ) (Set (Var "z")) ")" ) ")" ) ")" )))); theorem :: SEQ_4:93 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SEQ_4:94 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set (Var "n")))))) ; theorem :: SEQ_4:95 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:96 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" ($#k18_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:97 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "c")) ($#k20_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c")) ($#k17_complex1 :::".|"::: ) ) ($#k11_binop_2 :::"*"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) )))))) ; theorem :: SEQ_4:98 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z1")) ($#k22_seq_4 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z2")) ($#k22_seq_4 :::".|"::: ) ))))) ; theorem :: SEQ_4:99 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z1")) ($#k22_seq_4 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z2")) ($#k22_seq_4 :::".|"::: ) ))))) ; theorem :: SEQ_4:100 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z1")) ($#k22_seq_4 :::".|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z2")) ($#k22_seq_4 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:101 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z1")) ($#k22_seq_4 :::".|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z2")) ($#k22_seq_4 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:102 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) ")" ))) ; theorem :: SEQ_4:103 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set (Var "z2")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:104 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k22_seq_4 :::".|"::: ) )))) ; theorem :: SEQ_4:105 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k22_seq_4 :::".|"::: ) ))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n")) ")" ); attr "A" is :::"open"::: means :: SEQ_4:def 14 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") "st" (Bool (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "x")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) "A") ")" ) ")" ))); end; :: deftheorem defines :::"open"::: SEQ_4:def 14 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "x")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ))) ")" ))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n")) ")" ); attr "A" is :::"closed"::: means :: SEQ_4:def 15 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") "st" (Bool "(" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Set (Var "x")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) "A") ")" )) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")); end; :: deftheorem defines :::"closed"::: SEQ_4:def 15 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_seq_4 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Set (Var "x")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))); theorem :: SEQ_4:106 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ))) ; theorem :: SEQ_4:107 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ))) ; theorem :: SEQ_4:108 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "AA")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "AA")))) "holds" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "AA"))))) "holds" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) )))) ; theorem :: SEQ_4:109 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_seq_4 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "C")) "is" ($#v1_seq_4 :::"open"::: ) )))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); let "r" be ($#m1_subset_1 :::"Real":::); func :::"Ball"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) "n" ")" ) equals :: SEQ_4:def 16 "{" (Set (Var "z")) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") : (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k19_seq_4 :::"-"::: ) "x" ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "r") "}" ; end; :: deftheorem defines :::"Ball"::: SEQ_4:def 16 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k23_seq_4 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) : (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k19_seq_4 :::"-"::: ) (Set (Var "x")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )))); theorem :: SEQ_4:110 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k23_seq_4 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: SEQ_4:111 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k23_seq_4 :::"Ball"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; theorem :: SEQ_4:112 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) "holds" (Bool (Set ($#k23_seq_4 :::"Ball"::: ) "(" (Set (Var "z1")) "," (Set (Var "r1")) ")" ) "is" ($#v1_seq_4 :::"open"::: ) )))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n"))); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n")) ")" ); func :::"dist"::: "(" "x" "," "A" ")" -> ($#m1_subset_1 :::"Real":::) means :: SEQ_4:def 17 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set ($#k22_seq_4 :::"|."::: ) (Set "(" "x" ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") : (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "A") "}" )) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))))); end; :: deftheorem defines :::"dist"::: SEQ_4:def 17 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) : (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "}" )) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))))) ")" ))))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n")) ")" ); let "r" be ($#m1_subset_1 :::"Real":::); func :::"Ball"::: "(" "A" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) "n" ")" ) equals :: SEQ_4:def 18 "{" (Set (Var "z")) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") : (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "z")) "," "A" ")" ) ($#r1_xxreal_0 :::"<"::: ) "r") "}" ; end; :: deftheorem defines :::"Ball"::: SEQ_4:def 18 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k25_seq_4 :::"Ball"::: ) "(" (Set (Var "A")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) : (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) "}" )))); theorem :: SEQ_4:113 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "r9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r9")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r9"))) ")" )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))) ; theorem :: SEQ_4:114 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SEQ_4:115 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set "(" (Set (Var "x")) ($#k15_seq_4 :::"+"::: ) (Set (Var "z")) ")" ) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k22_seq_4 :::"|."::: ) (Set (Var "z")) ($#k22_seq_4 :::".|"::: ) )))))) ; theorem :: SEQ_4:116 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SEQ_4:117 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v2_seq_4 :::"closed"::: ) )) "holds" (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: SEQ_4:118 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z1")) "," (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k19_seq_4 :::"-"::: ) (Set (Var "x")) ")" ) ($#k22_seq_4 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "z1")) "," (Set (Var "A")) ")" ))))) ; theorem :: SEQ_4:119 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k25_seq_4 :::"Ball"::: ) "(" (Set (Var "A")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; theorem :: SEQ_4:120 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k25_seq_4 :::"Ball"::: ) "(" (Set (Var "A")) "," (Set (Var "r")) ")" )))))) ; theorem :: SEQ_4:121 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k25_seq_4 :::"Ball"::: ) "(" (Set (Var "A")) "," (Set (Var "r")) ")" ))))) ; theorem :: SEQ_4:122 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k25_seq_4 :::"Ball"::: ) "(" (Set (Var "A")) "," (Set (Var "r1")) ")" ) "is" ($#v1_seq_4 :::"open"::: ) )))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Const "n")) ")" ); func :::"dist"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Real":::) means :: SEQ_4:def 19 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) where x, z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) "n") : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" )) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))))); end; :: deftheorem defines :::"dist"::: SEQ_4:def 19 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) "{" (Set ($#k22_seq_4 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k19_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k22_seq_4 :::".|"::: ) ) where x, z "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" )) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))))) ")" )))); theorem :: SEQ_4:123 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SEQ_4:124 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) ; theorem :: SEQ_4:125 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k3_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "Y")) ")" )))) ; theorem :: SEQ_4:126 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )) ")" )) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "Y"))))) ; theorem :: SEQ_4:127 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SEQ_4:128 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" )))) ; theorem :: SEQ_4:129 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "A")) ")" ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k24_seq_4 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "B")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))))) ; theorem :: SEQ_4:130 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k26_seq_4 :::"dist"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"ComplexOpenSets"::: "n" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) "n" ")" ) equals :: SEQ_4:def 20 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) "n" ")" ) : (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) "}" ; end; :: deftheorem defines :::"ComplexOpenSets"::: SEQ_4:def 20 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k27_seq_4 :::"ComplexOpenSets"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) : (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) "}" )); theorem :: SEQ_4:131 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k27_seq_4 :::"ComplexOpenSets"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "A")) "is" ($#v1_seq_4 :::"open"::: ) ) ")" ))) ; theorem :: SEQ_4:132 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_seq_4 :::"COMPLEX"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_seq_4 :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_seq_4 :::"open"::: ) ) ")" ))) ; begin theorem :: SEQ_4:133 (Bool "for" (Set (Var "R")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ; theorem :: SEQ_4:134 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SEQ_4:135 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: SEQ_4:136 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))))))) ; theorem :: SEQ_4:137 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "v")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))))) ; theorem :: SEQ_4:138 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "v")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))))) ; theorem :: SEQ_4:139 (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "v")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "v1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "v")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Var "v1")) "is" ($#v5_valued_0 :::"increasing"::: ) ))) ; theorem :: SEQ_4:140 (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "v1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Var "v1")) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" ))) ; theorem :: SEQ_4:141 (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "v2")))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v2")))) & (Bool (Set (Var "v1")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "v2")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) ; definitionlet "v" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Incr"::: "v" -> ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQ_4:def 21 (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) "v")) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) "v" ")" ))) ")" ); end; :: deftheorem defines :::"Incr"::: SEQ_4:def 21 : (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k28_seq_4 :::"Incr"::: ) (Set (Var "v")))) "iff" (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "v")) ")" ))) ")" ) ")" ))); registrationlet "v" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k28_seq_4 :::"Incr"::: ) "v") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_valued_0 :::"increasing"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: SEQ_4:142 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B")) ")" ) ")" ))) ; theorem :: SEQ_4:143 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_xxreal_2 :::"bounded_above"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B")) ")" ) ")" ))) ; theorem :: SEQ_4:144 (Bool "for" (Set (Var "R")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r0"))) ")" )) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r0"))))) ;