:: LOPBAN_5  semantic presentation begin  
theorem :: LOPBAN_5:1 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k6_rinfsup1 :::"lim_inf"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k6_rinfsup1 :::"lim_inf"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: LOPBAN_5:2 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k5_rinfsup1 :::"lim_sup"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k5_rinfsup1 :::"lim_sup"::: )  (Set (Var "seq")) ")" ))))) ; 
 registrationlet "X" be   ($#l1_normsp_1 :::"RealBanachSpace":::); 
cluster (Set   ($#k2_normsp_2 :::"MetricSpaceNorm"::: )  "X") ->   ($#v4_tbsp_1 :::"complete"::: )   ; 
end; definitionlet "X" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "x0" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Ball":::  "(" "x0" "," "r" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: LOPBAN_5:def 1  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Point":::) "of" "X" : (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "x0"  ($#k5_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  "r")  "}"  ; end; 







:: deftheorem    defines :::"Ball"::: LOPBAN_5:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_lopban_5 :::"Ball"::: )   "(" (Set (Var "x0")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x0"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  "}"  )))); 
 
theorem :: LOPBAN_5:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "Y"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))) "is"   ($#v2_nfcont_1 :::"closed"::: )  )  ")" )) "holds"  (Bool  "ex" (Set (Var "n0")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )(Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set   ($#k1_lopban_5 :::"Ball"::: )   "(" (Set (Var "x0")) "," (Set (Var "r")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n0"))))  ")" )))))) ; 
 
theorem :: LOPBAN_5:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r5_nfcont_1 :::"is_Lipschitzian_on"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))) & (Bool (Set (Var "f"))  ($#r3_nfcont_1 :::"is_continuous_on"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "f"))  ($#r1_nfcont_1 :::"is_continuous_in"::: )  (Set (Var "x")))  ")" )  ")" ))) ; 
 
theorem :: LOPBAN_5:5 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "K")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "T")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "L"))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "T")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "L")))  ")" )  ")" ))))) ; 
 definitionlet "X", "Y" be   ($#l1_normsp_1 :::"RealNormSpace":::); let "H" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" )); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func "H" :::"#"::: "x" ->   ($#m1_subset_1 :::"sequence":::) "of" "Y" means :: LOPBAN_5:def 2 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "H"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k17_lopban_1 :::"."::: )  "x"))); end; 








:: deftheorem    defines :::"#"::: LOPBAN_5:def 2 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))))  ")" ))))); 
 
theorem :: LOPBAN_5:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  (Bool  "for" (Set (Var "vseq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "tseq")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Set (Var "tseq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x")) ")" )))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "tseq")) "is"   ($#v2_lopban_1 :::"Lipschitzian"::: )    ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "tseq"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_rinfsup1 :::"lim_inf"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "vseq")) ($#k4_normsp_0 :::".||"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" ) & (Bool  "("   "for" (Set (Var "ttseq")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "ttseq"))  ($#r1_hidden :::"="::: )  (Set (Var "tseq")))) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "ttseq")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_rinfsup1 :::"lim_inf"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "vseq")) ($#k4_normsp_0 :::".||"::: ) )))  ")" )  ")" ))))) ; 
 begin  
theorem :: LOPBAN_5:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "X0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "vseq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "X0")) "is"   ($#v1_tops_1 :::"dense"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X0")))) "holds"  (Bool (Set (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "K")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x")) ")" )  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )  ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  )))))) ; 
 
theorem :: LOPBAN_5:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_normsp_1 :::"RealBanachSpace":::)  (Bool  "for" (Set (Var "X0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_normsp_2 :::"LinearTopSpaceNorm"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "vseq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  "st" (Bool (Bool (Set (Var "X0")) "is"   ($#v1_tops_1 :::"dense"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X0")))) "holds"  (Bool (Set (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "K")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x")) ")" )  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "K")))  ")" )  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "tseq")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k16_lopban_1 :::"R_NormSpace_of_BoundedLinearOperators"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x"))) "is"   ($#v3_normsp_1 :::"convergent"::: )  ) & (Bool (Set (Set (Var "tseq"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_normsp_1 :::"lim"::: )  (Set  "(" (Set (Var "vseq"))  ($#k2_lopban_5 :::"#"::: )  (Set (Var "x")) ")" ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "tseq"))  ($#k17_lopban_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k6_rinfsup1 :::"lim_inf"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "vseq")) ($#k4_normsp_0 :::".||"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" )  ")" ) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "tseq")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_rinfsup1 :::"lim_inf"::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "vseq")) ($#k4_normsp_0 :::".||"::: ) )))  ")" ))))) ;