:: LP_SPACE  semantic presentation begin  definitionlet "x" be   ($#m1_subset_1 :::"Real_Sequence":::); let "p" be   ($#m1_subset_1 :::"Real":::); func "x" :::"rto_power"::: "p" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: LP_SPACE:def 1 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" "x"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  "p"))); end; 






:: deftheorem    defines :::"rto_power"::: LP_SPACE:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set (Var "p")))))  ")" )))); 
 definitionlet "p" be   ($#m1_subset_1 :::"Real":::); assume 
(Bool (Set (Const "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))
 ; func  :::"the_set_of_RealSequences_l^"::: "p" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) means :: LP_SPACE:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rsspace :::"the_set_of_RealSequences"::: )  )) & (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  "p") "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )); end; 






:: deftheorem    defines :::"the_set_of_RealSequences_l^"::: LP_SPACE:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "b2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rsspace :::"the_set_of_RealSequences"::: )  )) & (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" ))  ")" ))); 
 








theorem :: LP_SPACE:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b"))  ($#k4_power :::"to_power"::: )  (Set (Var "c"))))) ; 
 
theorem :: LP_SPACE:2 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_series_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "a"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "b"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ) ")" )))))) ; 
 
theorem :: LP_SPACE:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Set (Var "a"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set (Set (Var "b"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_series_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_series_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "a"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "b"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ) ")" )))  ")" ))) ; 
 
theorem :: LP_SPACE:4 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p"))) "is"   ($#v1_rlsub_1 :::"linearly-closed"::: )  )) ; 
 
theorem :: LP_SPACE:5 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: )  ))) ; 
 
theorem :: LP_SPACE:6 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "("  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v2_rlvect_1 :::"Abelian"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v3_rlvect_1 :::"add-associative"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v4_rlvect_1 :::"right_zeroed"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v13_algstr_0 :::"right_complementable"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v5_rlvect_1 :::"vector-distributive"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v6_rlvect_1 :::"scalar-distributive"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v7_rlvect_1 :::"scalar-associative"::: )  ) & (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#v8_rlvect_1 :::"scalar-unital"::: )  )  ")" )) ; 
 
theorem :: LP_SPACE:7 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "#)" ) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 definitionlet "p" be   ($#m1_subset_1 :::"Real":::); func  :::"l_norm^"::: "p" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p" ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: LP_SPACE:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p"))) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  "p" ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  "p" ")" )))); end; 





:: deftheorem    defines :::"l_norm^"::: LP_SPACE:def 3 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ))))  ")" ))); 
 
theorem :: LP_SPACE:8 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ) "is"   ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; 
 
theorem :: LP_SPACE:9 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: )  ))) ; 
 begin  
theorem :: LP_SPACE:10 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "lp")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )    "st" (Bool (Bool (Set (Var "lp"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "lp")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp"))) "iff" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Real_Sequence":::)) & (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )  ")" )  ")" ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "lp")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rsspace :::"Zeroseq"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x"))))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "y")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"   (Bool  "("  (Bool (Set   ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" ))) & (Bool (Set   ($#k2_rsspace :::"seq_id"::: )  (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "y")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "lp")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set  "("  ($#k2_rsspace :::"seq_id"::: )  (Set (Var "x")) ")" )  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: LP_SPACE:11 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "rseq"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "rseq"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: LP_SPACE:12 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Set (Var "rseq"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "(" (Set (Var "rseq"))  ($#k1_lp_space :::"rto_power"::: )  (Set (Var "p")) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "rseq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: LP_SPACE:13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "lp")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )    "st" (Bool (Bool (Set (Var "lp"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "lp"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "lp"))))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "lp"))))) "implies" (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )))  ")" ))))) ; 
 
theorem :: LP_SPACE:14 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "lp")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )    "st" (Bool (Bool (Set (Var "lp"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ))) "holds"  (Bool  "("  (Bool (Set (Var "lp")) "is"   ($#v4_normsp_0 :::"reflexive"::: )  ) & (Bool (Set (Var "lp")) "is"   ($#v3_normsp_0 :::"discerning"::: )  ) & (Bool (Set (Var "lp")) "is"   ($#v2_normsp_1 :::"RealNormSpace-like"::: )  )  ")" ))) ; 
 
theorem :: LP_SPACE:15 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "lp")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_1 :::"NORMSTR"::: )    "st" (Bool (Bool (Set (Var "lp"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ))) "holds"  (Bool (Set (Var "lp")) "is"   ($#l1_normsp_1 :::"RealNormSpace":::)))) ; 
 
theorem :: LP_SPACE:16 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool  "for" (Set (Var "lp")) "being"   ($#l1_normsp_1 :::"RealNormSpace":::)  "st" (Bool (Bool (Set (Var "lp"))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" ))) "holds"  (Bool  "for" (Set (Var "vseq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "lp"))  "st" (Bool (Bool (Set (Var "vseq")) "is"   ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: )  )) "holds"  (Bool (Set (Var "vseq")) "is"   ($#v3_normsp_1 :::"convergent"::: )  )))) ; 
 definitionlet "p" be   ($#m1_subset_1 :::"Real":::); assume 
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "p")))
 ; func  :::"l_Space^"::: "p" ->   ($#l1_normsp_1 :::"RealBanachSpace":::) equals :: LP_SPACE:def 4 (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p" ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p" ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p" ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  "p" ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  "p" ")" ) "#)" ); end; 






:: deftheorem    defines :::"l_Space^"::: LP_SPACE:def 4 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p")))) "holds"  (Bool (Set   ($#k4_lp_space :::"l_Space^"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_normsp_1 :::"NORMSTR"::: )  "(#"  (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  "("  ($#k10_rsspace :::"Zero_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k8_rsspace :::"Add_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k9_rsspace :::"Mult_"::: )   "(" (Set  "("  ($#k2_lp_space :::"the_set_of_RealSequences_l^"::: )  (Set (Var "p")) ")" ) "," (Set  ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")"  ")" ) "," (Set  "("  ($#k3_lp_space :::"l_norm^"::: )  (Set (Var "p")) ")" ) "#)" )));