:: TOPREALC semantic presentation begin theorem :: TOPREALC:1 (Bool "for" (Set (Var "X")) "being" ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_tarski :::"are_equipotent"::: ) )) "holds" (Bool (Set (Var "Y")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) ; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k3_square_1 :::"^2"::: ) ) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k3_square_1 :::"^2"::: ) ) -> ($#v2_xxreal_0 :::"positive"::: ) ; end; registration cluster (Set ($#k6_square_1 :::"sqrt"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v1_xboole_0 :::"zero"::: ) ; end; registrationlet "f" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k12_euclid :::"|."::: ) "f" ($#k12_euclid :::".|"::: ) ) -> ($#v1_xboole_0 :::"zero"::: ) ; end; theorem :: TOPREALC:2 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: TOPREALC:3 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: TOPREALC:4 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")))))) ; theorem :: TOPREALC:5 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k45_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")))))) ; theorem :: TOPREALC:6 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "c1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c1")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" ) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set "(" (Set (Var "c1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: TOPREALC:7 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")))))) ; theorem :: TOPREALC:8 (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "d")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))))) ; theorem :: TOPREALC:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k45_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k39_valued_1 :::"^2"::: ) ))) ; theorem :: TOPREALC:10 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ))))) ; theorem :: TOPREALC:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "s")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" ) ")" ))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "c" ")" ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; theorem :: TOPREALC:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "c")) ")" ")" ) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: TOPREALC:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))))) ; theorem :: TOPREALC:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n")))))) ; theorem :: TOPREALC:15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f1")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b2")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "f1")) "," (Set "(" (Set "(" ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" )))))) ; theorem :: TOPREALC:16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f1")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b2")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "f1")) "," (Set "(" (Set "(" ($#k16_euclid :::"0.REAL"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "r")) ")" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")))))))) ; theorem :: TOPREALC:17 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g1")) "being" ($#v1_valued_0 :::"complex-valued"::: ) (Set (Var "b2")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "g1")) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "c")) ")" ")" ) ($#k45_valued_1 :::"-"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "c")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "g1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" ))))) ; theorem :: TOPREALC:18 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))))) ; theorem :: TOPREALC:19 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: TOPREALC:20 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: TOPREALC:21 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set (Var "f")) ")" )))) ; theorem :: TOPREALC:22 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "B")) "being" (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "A")) ($#k6_struct_0 :::"-->"::: ) (Set (Var "t")))))))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n"))); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k6_waybel18 :::"proj"::: ) "(" (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) ($#k7_funcop_1 :::"-->"::: ) "T" ")" ) "," "i" ")" ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(/)"::: redefine func "p" :::"(/)"::: "r" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; theorem :: TOPREALC:23 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set (Var "r")) ")" )) ")" )))) ; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "S" is :::"complex-functions-membered"::: means :: TOPREALC:def 1 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "is" ($#v1_valued_2 :::"complex-functions-membered"::: ) ); attr "S" is :::"real-functions-membered"::: means :: TOPREALC:def 2 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "is" ($#v3_valued_2 :::"real-functions-membered"::: ) ); end; :: deftheorem defines :::"complex-functions-membered"::: TOPREALC:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_toprealc :::"complex-functions-membered"::: ) ) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "is" ($#v1_valued_2 :::"complex-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"real-functions-membered"::: TOPREALC:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_toprealc :::"real-functions-membered"::: ) ) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "is" ($#v3_valued_2 :::"real-functions-membered"::: ) ) ")" )); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) "n") -> ($#v2_toprealc :::"real-functions-membered"::: ) ; end; registration cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v3_topmetr :::"real-membered"::: ) ; end; registration cluster (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registration cluster ($#v2_toprealc :::"real-functions-membered"::: ) -> ($#v1_toprealc :::"complex-functions-membered"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registration cluster ($#v1_struct_0 :::"strict"::: ) ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_toprealc :::"real-functions-membered"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end; registrationlet "S" be ($#v1_toprealc :::"complex-functions-membered"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registrationlet "S" be ($#v2_toprealc :::"real-functions-membered"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_toprealc :::"real-functions-membered"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "S" be ($#v1_toprealc :::"complex-functions-membered"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v1_toprealc :::"complex-functions-membered"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "S"; end; registrationlet "S" be ($#v2_toprealc :::"real-functions-membered"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster -> ($#v2_toprealc :::"real-functions-membered"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "S"; end; definitionlet "X" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; func :::"(-)"::: "X" -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) means :: TOPREALC:def 3 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) "X") ")" )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) ")" ))) ; end; :: deftheorem defines :::"(-)"::: TOPREALC:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_toprealc :::"(-)"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )); registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_toprealc :::"(-)"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_toprealc :::"(-)"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; theorem :: TOPREALC:24 (Bool "for" (Set (Var "X")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_toprealc :::"(-)"::: ) (Set (Var "X")))) ")" ))) ; registrationlet "X" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_toprealc :::"(-)"::: ) "X") -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; theorem :: TOPREALC:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k2_rltopsp1 :::"-"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_toprealc :::"(-)"::: ) (Set (Var "X")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"(-)"::: redefine func :::"(-)"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k2_toprealc :::"(-)"::: ) "X") -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "p" :::"."::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "R", "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "T")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k2_borsuk_1 :::":]"::: ) ); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m1_subset_1 :::"Point":::) "of" "T"; end; definitionlet "R", "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "T")); let "r" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "R")); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); :: original: :::"."::: redefine func "f" :::"."::: "(" "r" "," "s" ")" -> ($#m1_subset_1 :::"Point":::) "of" "T"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "p" :::"+"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "p" :::"-"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "p" :::"(#)"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(/)"::: redefine func "p" :::"(/)"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"(#)"::: redefine func "p1" :::"(#)"::: "p2" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); commutativity (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ) "holds" (Bool (Set (Set (Var "p1")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "p1"))))) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"^2"::: redefine func :::"sqr"::: "p" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); :: original: :::"/""::: redefine func "p1" :::"/""::: "p2" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "x" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+*"::: redefine func "p" :::"+*"::: "(" "x" "," "r" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; theorem :: TOPREALC:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "o")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r"))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k14_euclid :::"Euclid"::: ) "n") -> ($#v2_toprealc :::"real-functions-membered"::: ) ; end; theorem :: TOPREALC:27 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: TOPREALC:28 (Bool "for" (Set (Var "V")) "being" ($#~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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: TOPREALC:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" ))))))) ; theorem :: TOPREALC:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" ))))))) ; theorem :: TOPREALC:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k42_valued_2 :::"[#]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" ))))))) ; theorem :: TOPREALC:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k48_valued_2 :::"[/]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k69_valued_2 :::""::: ) (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" ))))))) ; registrationlet "D" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); cluster (Set "f" ($#k72_valued_2 :::"<++>"::: ) "g") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; cluster (Set "f" ($#k78_valued_2 :::"<-->"::: ) "g") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; cluster (Set "f" ($#k83_valued_2 :::"<##>"::: ) "g") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; cluster (Set "f" ($#k89_valued_2 :::""::: ) "g") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: TOPREALC:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k17_valued_2 :::"<->"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREALC:34 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; theorem :: TOPREALC:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k32_valued_2 :::"[+]"::: ) (Set (Var "r"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k38_valued_2 :::"[-]"::: ) (Set (Var "r"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k43_valued_2 :::"[#]"::: ) (Set (Var "r"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k49_valued_2 :::"[/]"::: ) (Set (Var "r"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k74_valued_2 :::"<++>"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREALC:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k80_valued_2 :::"<-->"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREALC:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k85_valued_2 :::"<##>"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREALC:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k91_valued_2 :::""::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; theorem :: TOPREALC:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k53_valued_2 :::"<+>"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k59_valued_2 :::"<->"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k64_valued_2 :::"<#>"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: TOPREALC:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k70_valued_2 :::""::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "R")); func :::"incl"::: "(" "f" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) means :: TOPREALC:def 4 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "T" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set "n" ($#k2_finseq_2 :::"|->"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" )))); end; :: deftheorem defines :::"incl"::: TOPREALC:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "R")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" )))) ")" )))))); theorem :: TOPREALC:47 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "R")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "R")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k4_toprealc :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))))))))) ; theorem :: TOPREALC:48 (Bool "for" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "R")) "holds" (Bool (Set ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "T")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: TOPREALC:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k53_valued_2 :::"<+>"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k74_valued_2 :::"<++>"::: ) (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: TOPREALC:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k59_valued_2 :::"<->"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k80_valued_2 :::"<-->"::: ) (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: TOPREALC:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k64_valued_2 :::"<#>"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k85_valued_2 :::"<##>"::: ) (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ))))))) ; theorem :: TOPREALC:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k70_valued_2 :::""::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k91_valued_2 :::""::: ) (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ))))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"TIMES"::: "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) means :: TOPREALC:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "holds" (Bool (Set it ($#k6_toprealc :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_toprealc :::"(#)"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"TIMES"::: TOPREALC:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_toprealc :::"TIMES"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k6_toprealc :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_toprealc :::"(#)"::: ) (Set (Var "y"))))) ")" ))); theorem :: TOPREALC:53 (Bool (Set ($#k16_toprealc :::"TIMES"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) ($#k6_struct_0 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))) ; theorem :: TOPREALC:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k85_valued_2 :::"<##>"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_toprealc :::"TIMES"::: ) (Set (Var "n")) ")" ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))))) ; definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); func :::"PROJ"::: "(" "m" "," "n" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "m" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: TOPREALC:def 6 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "m" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) "n"))); end; :: deftheorem defines :::"PROJ"::: TOPREALC:def 6 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_toprealc :::"PROJ"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))))) ")" ))); theorem :: TOPREALC:55 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k17_toprealc :::"PROJ"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))))) ; theorem :: TOPREALC:56 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k17_toprealc :::"PROJ"::: ) "(" (Set (Var "m")) "," (Set (Var "m")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k15_toprealc :::"incl"::: ) "(" (Set (Var "f")) "," (Set (Var "m")) ")" ")" )))))) ; begin registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ))) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: TOPREALC:57 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k17_toprealc :::"PROJ"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) )) ; theorem :: TOPREALC:58 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k17_toprealc :::"PROJ"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v1_t_0topsp :::"open"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set ($#k15_toprealc :::"incl"::: ) "(" "f" "," "n" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k16_toprealc :::"TIMES"::: ) "n") -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPREALC:59 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k14_valued_2 :::"(/)"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f", "g" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); let "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k50_valued_1 :::"/""::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f", "g" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set "f" ($#k72_valued_2 :::"<++>"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k78_valued_2 :::"<-->"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k83_valued_2 :::"<##>"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "g" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k51_valued_2 :::"<+>"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k57_valued_2 :::"<->"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k62_valued_2 :::"<#>"::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); cluster (Set "f" ($#k68_valued_2 :::""::: ) "g") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set "f" ($#k30_valued_2 :::"[+]"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k36_valued_2 :::"[-]"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k41_valued_2 :::"[#]"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); cluster (Set "f" ($#k47_valued_2 :::"[/]"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ); end; theorem :: TOPREALC:60 (Bool "for" (Set (Var "r")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "p"))) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ))))) ; theorem :: TOPREALC:61 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "r" be ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Const "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Const "r")) ")" ")" ); :: original: :::"(-)"::: redefine func :::"(-)"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," "r" ")" ")" ); end; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "r" be ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Const "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Const "r")) ")" ")" ); cluster (Set ($#k2_toprealc :::"(-)"::: ) "X") -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" "m" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," "r" ")" ")" ); end; theorem :: TOPREALC:62 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ))))) ;