:: MAZURULM  semantic presentation begin  


















registration
cluster (Set   ($#k17_borsuk_1 :::"I[01]"::: )  ) ->   ($#v1_borsuk_1 :::"closed"::: )    for   ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k3_topmetr :::"R^1"::: )  ); 
end; 
theorem :: MAZURULM:1 (Bool (Set   ($#k2_urysohn1 :::"DYADIC"::: )  ) "is"   ($#v1_tops_1 :::"dense"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )) ; 
 
theorem :: MAZURULM:2 (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  ($#k2_urysohn1 :::"DYADIC"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_xxreal_1 :::".]"::: ) )) ; 
 
theorem :: MAZURULM:3 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "a")))))) ; 
 
theorem :: MAZURULM:4 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 registrationlet "A" be   ($#v3_membered :::"real-membered"::: )     ($#v4_xxreal_2 :::"bounded_above"::: )     ($#m1_hidden :::"set"::: )  ; let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k23_member_1 :::"**"::: )  "A") ->   ($#v4_xxreal_2 :::"bounded_above"::: )   ; 
end; registrationlet "A" be   ($#v3_membered :::"real-membered"::: )     ($#v4_xxreal_2 :::"bounded_above"::: )     ($#m1_hidden :::"set"::: )  ; let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k23_member_1 :::"**"::: )  "A") ->   ($#v3_xxreal_2 :::"bounded_below"::: )   ; 
end; registrationlet "A" be   ($#v3_membered :::"real-membered"::: )     ($#v3_xxreal_2 :::"bounded_below"::: )     ($#m1_hidden :::"set"::: )  ; let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k23_member_1 :::"**"::: )  "A") ->   ($#v3_xxreal_2 :::"bounded_below"::: )   ; 
end; registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_membered :::"real-membered"::: )     ($#v3_xxreal_2 :::"bounded_below"::: )     ($#m1_hidden :::"set"::: )  ; let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k23_member_1 :::"**"::: )  "A") ->   ($#v4_xxreal_2 :::"bounded_above"::: )   ; 
end; 
theorem :: MAZURULM:5 (Bool  "for" (Set (Var "t")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "t")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "t"))  ($#k9_valued_1 :::"+"::: )  (Set (Var "f")))))) ; 
 
theorem :: MAZURULM:6 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 
theorem :: MAZURULM:7 (Bool  "for" (Set (Var "t")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "t"))  ($#k9_valued_1 :::"+"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k9_binop_2 :::"+"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "f")) ")" ))))) ; 
 registrationlet "f" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); let "t" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "t"  ($#k7_valued_1 :::"+"::: )  "f") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: MAZURULM:8 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_ndiff_1 :::"(#)"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "a")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k2_ndiff_1 :::"*"::: )  (Set (Var "a"))))))) ; 
 
theorem :: MAZURULM:9 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k8_funcop_1 :::"-->"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: MAZURULM:10 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "f"))  ($#k2_ndiff_1 :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "f")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "a"))))))) ; 
 registrationlet "f" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); let "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "E")); 
cluster (Set "f"  ($#k2_ndiff_1 :::"*"::: )  "a") ->   ($#v3_normsp_1 :::"convergent"::: )   ; 
end; definitionlet "E", "F" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "F")); attr "f" is  :::"isometric":::  means :: MAZURULM:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "E" "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))); end; 






:: deftheorem    defines :::"isometric"::: MAZURULM:def 1 :  (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_mazurulm :::"isometric"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))  ")" ))); 
 definitionlet "E", "F" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "F")); attr "f" is  :::"Affine":::  means :: MAZURULM:def 2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "E"  (Bool  "for" (Set (Var "t")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set (Var "t")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set (Var "t")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" ))))); attr "f" is  :::"midpoints-preserving":::  means :: MAZURULM:def 3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "E" "holds"  (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" )))); end; 












:: deftheorem    defines :::"Affine"::: MAZURULM:def 2 :  (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_mazurulm :::"Affine"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "t")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t"))) & (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set (Var "t")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 1)  ($#k10_binop_2 :::"-"::: )  (Set (Var "t")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" )))))  ")" ))); 
 
:: deftheorem    defines :::"midpoints-preserving"::: MAZURULM:def 3 :  (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k18_binop_2 :::"/"::: )  (Num 2) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" ) ")" ))))  ")" ))); 
 registrationlet "E" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )  ; 
cluster (Set   ($#k3_struct_0 :::"id"::: )  "E") ->   ($#v1_mazurulm :::"isometric"::: )   ; 
end; registrationlet "E" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; 
cluster (Set   ($#k3_struct_0 :::"id"::: )  "E") ->   ($#v2_mazurulm :::"Affine"::: )     ($#v3_mazurulm :::"midpoints-preserving"::: )   ; 
end; registrationlet "E" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E")) bbbadV5_RELAT_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E"))   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v3_funct_2 :::"bijective"::: )     ($#v1_mazurulm :::"isometric"::: )     ($#v2_mazurulm :::"Affine"::: )     ($#v3_mazurulm :::"midpoints-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E"))))); 
end; 
theorem :: MAZURULM:11 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "G")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set (Var "G"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_mazurulm :::"isometric"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v1_mazurulm :::"isometric"::: )  )) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v1_mazurulm :::"isometric"::: )  )))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be   ($#v1_mazurulm :::"isometric"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "g"  ($#k3_relat_1 :::"*"::: )  "f") ->   ($#v1_mazurulm :::"isometric"::: )    for  ($#m1_subset_1 :::"UnOp":::) "of" "E"; 
end; 
theorem :: MAZURULM:12 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_mazurulm :::"isometric"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"/""::: )  ) "is"   ($#v1_mazurulm :::"isometric"::: )  ))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#v3_funct_2 :::"bijective"::: )     ($#v1_mazurulm :::"isometric"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "f"  ($#k2_tops_2 :::"/""::: )  ) ->   ($#v1_mazurulm :::"isometric"::: )   ; 
end; 
theorem :: MAZURULM:13 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "G")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set (Var "G"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  )) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  )))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be   ($#v3_mazurulm :::"midpoints-preserving"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "g"  ($#k3_relat_1 :::"*"::: )  "f") ->   ($#v3_mazurulm :::"midpoints-preserving"::: )    for  ($#m1_subset_1 :::"UnOp":::) "of" "E"; 
end; 
theorem :: MAZURULM:14 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"/""::: )  ) "is"   ($#v3_mazurulm :::"midpoints-preserving"::: )  ))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#v3_funct_2 :::"bijective"::: )     ($#v3_mazurulm :::"midpoints-preserving"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "f"  ($#k2_tops_2 :::"/""::: )  ) ->   ($#v3_mazurulm :::"midpoints-preserving"::: )   ; 
end; 
theorem :: MAZURULM:15 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "G")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set (Var "G"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_mazurulm :::"Affine"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_mazurulm :::"Affine"::: )  )) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v2_mazurulm :::"Affine"::: )  )))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be   ($#v2_mazurulm :::"Affine"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "g"  ($#k3_relat_1 :::"*"::: )  "f") ->   ($#v2_mazurulm :::"Affine"::: )    for  ($#m1_subset_1 :::"UnOp":::) "of" "E"; 
end; 
theorem :: MAZURULM:16 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_funct_2 :::"bijective"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_mazurulm :::"Affine"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"/""::: )  ) "is"   ($#v2_mazurulm :::"Affine"::: )  ))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be   ($#v3_funct_2 :::"bijective"::: )     ($#v2_mazurulm :::"Affine"::: )    ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "E")); 
cluster (Set "f"  ($#k2_tops_2 :::"/""::: )  ) ->   ($#v2_mazurulm :::"Affine"::: )   ; 
end; definitionlet "E" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "E")); func "a" :::"-reflection":::  ->   ($#m1_subset_1 :::"UnOp":::) "of" "E" means :: MAZURULM:def 4 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "E" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_rlvect_1 :::"*"::: )  "a" ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b"))))); end; 






:: deftheorem    defines :::"-reflection"::: MAZURULM:def 4 :  (Bool  "for" (Set (Var "E")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  )) "iff" (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")))))  ")" )))); 
 
theorem :: MAZURULM:17 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "E")))))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "E")); 
cluster (Set "a"  ($#k1_mazurulm :::"-reflection"::: )  ) ->   ($#v3_funct_2 :::"bijective"::: )   ; 
end; 
theorem :: MAZURULM:18 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )  ")" ))) ; 
 
theorem :: MAZURULM:19 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")))))) ; 
 
theorem :: MAZURULM:20 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "a")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "b"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "a")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))) ; 
 
theorem :: MAZURULM:21 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: MAZURULM:22 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k11_binop_2 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "b"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "a")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))))) ; 
 
theorem :: MAZURULM:23 (Bool  "for" (Set (Var "E")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "E")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  ")" )  ($#k2_tops_2 :::"/""::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "a"))  ($#k1_mazurulm :::"-reflection"::: )  )))) ; 
 registrationlet "E" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "E")); 
cluster (Set "a"  ($#k1_mazurulm :::"-reflection"::: )  ) ->   ($#v1_mazurulm :::"isometric"::: )   ; 
end; 
theorem :: MAZURULM:24 (Bool  "for" (Set (Var "E")) "," (Set (Var "F")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "F"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_mazurulm :::"isometric"::: )  )) "holds"  (Bool (Set (Var "f"))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) ; 
 registrationlet "E", "F" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v3_funct_2 :::"bijective"::: )     ($#v1_mazurulm :::"isometric"::: )    ->   ($#v3_mazurulm :::"midpoints-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))))); 
end; registrationlet "E", "F" be   ($#l1_normsp_1 :::"RealNormSpace":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_mazurulm :::"isometric"::: )     ($#v3_mazurulm :::"midpoints-preserving"::: )    ->   ($#v2_mazurulm :::"Affine"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "E") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "F"))))); 
end;