:: MFOLD_2  semantic presentation begin  registration
cluster (Set   ($#k1_xboole_0 :::"{}"::: )  ) -> (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#v5_relat_1 :::"-valued"::: )   ; 

cluster (Set   ($#k1_xboole_0 :::"{}"::: )  ) ->   ($#v2_funct_2 :::"onto"::: )   ; 
end; 
theorem :: MFOLD_2:1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "Y"))  ($#k6_relat_1 :::"|`"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set (Var "Y")))))) ; 
 
theorem :: MFOLD_2:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y2"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1")))) "holds"  (Bool (Set (Set  "(" (Set (Var "Y1"))  ($#k6_relat_1 :::"|`"::: )  (Set (Var "f")) ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "Y2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set (Var "Y2")))))) ; 
 
theorem :: MFOLD_2:3 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  ) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 definitionlet "S", "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; :: original: :::"are_homeomorphic"::: redefine pred "S" "," "T" :::"are_homeomorphic"::: ; symmetry  
(Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool bbbadR1_T_0TOPSP((Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool bbbadR1_T_0TOPSP((Set (Var "b2")) "," (Set (Var "b1")))))
 ; end; 














theorem :: MFOLD_2:4 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "T1"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set (Var "A2")) ")" ) ")" ) "," (Set  "(" (Set (Var "T2"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A2")) ")" )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A2"))  ($#k6_relset_1 :::"|`"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))))) ; 
 
theorem :: MFOLD_2:5 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set (Var "A2"))) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )))) ; 
 
theorem :: MFOLD_2:6 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "A2")) "," (Set (Var "A1"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )))) ; 
 
theorem :: MFOLD_2:7 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "iff" (Bool (Set (Var "A2")) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )))) ; 
 
theorem :: MFOLD_2:8 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "T3")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  (Bool  "for" (Set (Var "A3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T3"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  ) & (Bool (Set (Var "A2")) "," (Set (Var "A3"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "A1")) "," (Set (Var "A3"))  ($#r1_metrizts :::"are_homeomorphic"::: )  ))))) ; 
 
theorem :: MFOLD_2:9 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Var "T1")) "," (Set (Var "T2"))  ($#r1_mfold_2 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "T2")) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) ; 
 








theorem :: MFOLD_2:10 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v8_pre_topc :::"Hausdorff"::: )  ) & (Bool (Set (Var "M")) "," (Set (Var "N"))  ($#r1_mfold_2 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "N")) "is"   ($#v8_pre_topc :::"Hausdorff"::: )  )) ; 
 
theorem :: MFOLD_2:11 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "M")) "is" (Set (Var "n"))  ($#v2_mfold_1 :::"-locally_euclidean"::: )  ) & (Bool (Set (Var "M")) "," (Set (Var "N"))  ($#r1_mfold_2 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "N")) "is" (Set (Var "n"))  ($#v2_mfold_1 :::"-locally_euclidean"::: )  ))) ; 
 
theorem :: MFOLD_2:12 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "M")) "is" (Set (Var "n"))  ($#v3_mfold_1 :::"-manifold"::: )  ) & (Bool (Set (Var "M")) "," (Set (Var "N"))  ($#r1_mfold_2 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "N")) "is" (Set (Var "n"))  ($#v3_mfold_1 :::"-manifold"::: )  ))) ; 
 
theorem :: MFOLD_2:13 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (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   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "x2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))) & (Bool (Set (Set  "("  ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set (Var "x2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")" ))) ; 
 
theorem :: MFOLD_2:14 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y2"))))) "holds"  (Bool (Set   ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set  "(" (Set (Var "x1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "x2"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "y2")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "x1")) "," (Set (Var "x2")) ")"  ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "("  ($#k14_rvsum_1 :::"mlt"::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")"  ")" )))) ; 
 
theorem :: MFOLD_2:15 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y2"))))) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set  "(" (Set (Var "x1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "x2"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) )  ($#k9_binop_2 :::"+"::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; 
 









theorem :: MFOLD_2:16 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set (Var "p2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: MFOLD_2:17 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))) "iff" (Bool (Set (Var "X")) "is"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n"))))  ")" ))) ; 
 
theorem :: MFOLD_2:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "fr")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Fv")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) ")" )  (Bool  "for" (Set (Var "fv")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "fr"))  ($#r1_funct_2 :::"="::: )  (Set (Var "fv"))) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "Fv")))) "holds"  (Bool (Set (Set (Var "fr"))  ($#k5_rlvect_2 :::"(#)"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fv"))  ($#k5_rlvect_2 :::"(#)"::: )  (Set (Var "Fv"))))))))) ; 
 
theorem :: MFOLD_2:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Fv")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "Fv"))  ($#r1_hidden :::"="::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set (Var "Fv"))))))) ; 
 
theorem :: MFOLD_2:20 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Lv")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))  (Bool  "for" (Set (Var "Lr")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set (Var "Lr"))  ($#r1_funct_2 :::"="::: )  (Set (Var "Lv")))) "holds"  (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "Lr")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "Lv"))))))) ; 
 
theorem :: MFOLD_2:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k10_funcsdom :::"RealVectSpace"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) ")" )  (Bool  "for" (Set (Var "Ar")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "Af"))  ($#r1_hidden :::"="::: )  (Set (Var "Ar")))) "holds"  (Bool  "("  (Bool (Set (Var "Af")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) "iff" (Bool (Set (Var "Ar")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )  ")" )))) ; 
 
theorem :: MFOLD_2:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "V"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_euclid_7 :::"RN_Base"::: )  (Set (Var "n"))))) "holds"  (Bool  "ex" (Set (Var "l")) "being"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")))))))) ; 
 
theorem :: MFOLD_2:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k8_euclid_7 :::"RN_Base"::: )  (Set (Var "n"))) "is"    ($#m1_rlvect_3 :::"Basis"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n"))))) ; 
 
theorem :: MFOLD_2:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) & (Bool (Set   ($#k1_topreal9 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "V")))  ")" )))  ")" ))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"InnerProduct"::: "p" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) means :: MFOLD_2:def 1 (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) "p" "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))); end; 






:: deftheorem    defines :::"InnerProduct"::: MFOLD_2:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_mfold_2 :::"InnerProduct"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) )))  ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set   ($#k1_mfold_2 :::"InnerProduct"::: )  "p") ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "p", "q" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"Plane":::  "(" "p" "," "q" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) equals :: MFOLD_2:def 2  "{"  (Set (Var "y")) where y "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) : (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) "p" "," (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  "q" ")" ) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  "}"  ; end; 







:: deftheorem    defines :::"Plane"::: MFOLD_2:def 2 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "y")) where y "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set  "(" (Set (Var "y"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  "}"  ))); 
 
theorem :: MFOLD_2:25 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_rltopsp1 :::"transl"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p")) "," (Set (Var "p2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p")) "," (Set  "(" (Set (Var "p1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "p2")) ")" ) ")" )))) ; 
 
theorem :: MFOLD_2:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#v1_rlvect_3 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k10_binop_2 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) ")" ))  ")" )))) ; 
 
theorem :: MFOLD_2:27 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool  "ex" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "R"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p1")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p2")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) ")" ))  ")" )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "p", "q" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"TPlane":::  "(" "p" "," "q" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") equals :: MFOLD_2:def 3 (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_mfold_2 :::"Plane"::: )   "(" "p" "," "q" ")"  ")" )); end; 







:: deftheorem    defines :::"TPlane"::: MFOLD_2:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k3_mfold_2 :::"TPlane"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_mfold_2 :::"Plane"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")"  ")" ))))); 
 
theorem :: MFOLD_2:28 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_euclid_7 :::"Base_FinSeq"::: )   "(" (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: MFOLD_2:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )))) "holds"  (Bool (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n"))) "," (Set   ($#k3_mfold_2 :::"TPlane"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_mfold_2 :::"are_homeomorphic"::: )  ))) ; 
 
theorem :: MFOLD_2:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")" )))) "holds"  (Bool (Set   ($#k3_mfold_2 :::"TPlane"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" (Set (Var "n"))  ($#v3_mfold_1 :::"-manifold"::: )  ))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"TUnitSphere"::: "n" ->   ($#l1_pre_topc :::"TopSpace":::) equals :: MFOLD_2:def 4 (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Set  "(" "n"  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )); end; 





:: deftheorem    defines :::"TUnitSphere"::: MFOLD_2:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_mfold_2 :::"TUnitSphere"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Set  "(" (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_mfold_2 :::"TUnitSphere"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "S" be    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n"))); assume 
(Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) ")" ) "," (Num 1) ")" ))
 ; func  :::"stereographic_projection":::  "(" "S" "," "p" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "S" "," (Set  "("  ($#k3_mfold_2 :::"TPlane"::: )   "(" "p" "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) ")" ) ")"  ")" ) means :: MFOLD_2:def 5 (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_struct_0 :::"in"::: )  "S")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," "p" ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," "p" ($#k23_rvsum_1 :::")|"::: ) )  ($#k1_rlvect_1 :::"*"::: )  "p" ")" ) ")" )))); end; 








:: deftheorem    defines :::"stereographic_projection"::: MFOLD_2:def 5 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "S")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")" ))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set  "("  ($#k3_mfold_2 :::"TPlane"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_mfold_2 :::"stereographic_projection"::: )   "(" (Set (Var "S")) "," (Set (Var "p")) ")" )) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_struct_0 :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k12_binop_2 :::"/"::: )  (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "p")) ")" ) ")" ))))  ")" ))))); 
 
theorem :: MFOLD_2:31 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "S")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")"  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")" ))) "holds"  (Bool (Set   ($#k5_mfold_2 :::"stereographic_projection"::: )   "(" (Set (Var "S")) "," (Set (Var "p")) ")" ) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k4_mfold_2 :::"TUnitSphere"::: )  "n") ->   ($#v5_waybel23 :::"second-countable"::: )   ; 

cluster (Set   ($#k4_mfold_2 :::"TUnitSphere"::: )  "n") -> "n"  ($#v2_mfold_1 :::"-locally_euclidean"::: )   ; 

cluster (Set   ($#k4_mfold_2 :::"TUnitSphere"::: )  "n") -> "n"  ($#v3_mfold_1 :::"-manifold"::: )   ; 
end;