:: REAL_NS1 semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Euclid_add"::: "n" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) means :: REAL_NS1:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_euclid :::"+"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"Euclid_add"::: REAL_NS1:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_ns1 :::"Euclid_add"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_euclid :::"+"::: ) (Set (Var "b"))))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_real_ns1 :::"Euclid_add"::: ) "n") -> ($#v1_binop_1 :::"commutative"::: ) ($#v2_binop_1 :::"associative"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Euclid_mult"::: "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) means :: REAL_NS1:def 2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x")))))); end; :: deftheorem defines :::"Euclid_mult"::: REAL_NS1:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_real_ns1 :::"Euclid_mult"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_euclid :::"*"::: ) (Set (Var "x")))))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Euclid_norm"::: "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: REAL_NS1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))); end; :: deftheorem defines :::"Euclid_norm"::: REAL_NS1:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_real_ns1 :::"Euclid_norm"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"REAL-NS"::: "n" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) means :: REAL_NS1:def 4 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) "n")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k1_real_ns1 :::"Euclid_add"::: ) "n")) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k2_real_ns1 :::"Euclid_mult"::: ) "n")) & (Bool (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k3_real_ns1 :::"Euclid_norm"::: ) "n")) ")" ); end; :: deftheorem defines :::"REAL-NS"::: REAL_NS1:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k1_real_ns1 :::"Euclid_add"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k2_real_ns1 :::"Euclid_mult"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k3_real_ns1 :::"Euclid_norm"::: ) (Set (Var "n")))) ")" ) ")" ))); registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k4_real_ns1 :::"REAL-NS"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ; end; theorem :: REAL_NS1:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: REAL_NS1:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_euclid :::"+"::: ) (Set (Var "b"))))))) ; theorem :: REAL_NS1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "y")))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k4_real_ns1 :::"REAL-NS"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v1_normsp_1 :::"strict"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; theorem :: REAL_NS1:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid :::"-"::: ) (Set (Var "a"))))))) ; theorem :: REAL_NS1:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_euclid :::"-"::: ) (Set (Var "b"))))))) ; theorem :: REAL_NS1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))))) ; theorem :: REAL_NS1:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "x")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: REAL_NS1:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: REAL_NS1:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "y")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))))) ; theorem :: REAL_NS1:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); let "k" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "f" :::"."::: "k" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; theorem :: REAL_NS1:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "xs")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "xseq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "xs")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "xseq")) ($#r1_funct_2 :::"="::: ) (Set (Var "seq")))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "rseqi")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "rseqi")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "xseq")) ($#k5_real_ns1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "rseqi")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Set (Var "xs")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseqi")))) ")" )))) ")" )))))) ; theorem :: REAL_NS1:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v3_normsp_1 :::"convergent"::: ) ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k4_real_ns1 :::"REAL-NS"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#v3_lopban_1 :::"complete"::: ) ; end; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Euclid_scalar"::: "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: REAL_NS1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))); end; :: deftheorem defines :::"Euclid_scalar"::: REAL_NS1:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"REAL-US"::: "n" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_bhsp_1 :::"strict"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) means :: REAL_NS1:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) "n")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) "n")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k1_real_ns1 :::"Euclid_add"::: ) "n")) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k2_real_ns1 :::"Euclid_mult"::: ) "n")) & (Bool (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k6_real_ns1 :::"Euclid_scalar"::: ) "n")) ")" ); end; :: deftheorem defines :::"REAL-US"::: REAL_NS1:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_bhsp_1 :::"strict"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k1_real_ns1 :::"Euclid_add"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k2_real_ns1 :::"Euclid_mult"::: ) (Set (Var "n")))) & (Bool (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")))) ")" ) ")" ))); registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_real_ns1 :::"REAL-US"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_bhsp_1 :::"strict"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_real_ns1 :::"REAL-US"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v1_bhsp_1 :::"strict"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ; end; theorem :: REAL_NS1:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool "(" (Bool (Set (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y2")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")))) ")" ))))) ; theorem :: REAL_NS1:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x1")) ($#k1_normsp_0 :::".||"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x2"))))))) ; theorem :: REAL_NS1:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" )) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" )) ")" ))) ; theorem :: REAL_NS1:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "seq1")) ($#r1_funct_2 :::"="::: ) (Set (Var "seq2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "implies" (Bool "(" (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2")))) ")" ) ")" & "(" (Bool (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "implies" (Bool "(" (Bool (Set (Var "seq1")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq2")))) ")" ) ")" ")" )))) ; theorem :: REAL_NS1:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "seq1")) ($#r1_funct_2 :::"="::: ) (Set (Var "seq2"))) & (Bool (Set (Var "seq1")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )) "holds" (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_3 :::"Cauchy"::: ) )))) ; theorem :: REAL_NS1:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_real_ns1 :::"REAL-NS"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "seq1")) ($#r1_funct_2 :::"="::: ) (Set (Var "seq2"))) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_3 :::"Cauchy"::: ) )) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_real_ns1 :::"REAL-US"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_bhsp_1 :::"strict"::: ) ($#v3_bhsp_3 :::"complete"::: ) ; end;