:: RSSPACE semantic presentation begin definitionfunc :::"the_set_of_RealSequences"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: RSSPACE:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real_Sequence":::)) ")" )); end; :: deftheorem defines :::"the_set_of_RealSequences"::: RSSPACE:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real_Sequence":::)) ")" )) ")" )); definitionlet "a" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) )) ; func :::"seq_id"::: "a" -> ($#m1_subset_1 :::"Real_Sequence":::) equals :: RSSPACE:def 2 "a"; end; :: deftheorem defines :::"seq_id"::: RSSPACE:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ))) "holds" (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))); definitionlet "a" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; func :::"R_id"::: "a" -> ($#m1_subset_1 :::"Real":::) equals :: RSSPACE:def 3 "a"; end; :: deftheorem defines :::"R_id"::: RSSPACE:def 3 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set ($#k3_rsspace :::"R_id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))); definitionfunc :::"l_add"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) means :: RSSPACE:def 4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "a")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "b")) ")" )))); end; :: deftheorem defines :::"l_add"::: RSSPACE:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_rsspace :::"l_add"::: ) )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "a")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "b")) ")" )))) ")" )); definitionfunc :::"l_mult"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) means :: RSSPACE:def 5 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rsspace :::"R_id"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"l_mult"::: RSSPACE:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_rsspace :::"l_mult"::: ) )) "iff" (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rsspace :::"R_id"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" )))) ")" )); definitionfunc :::"Zeroseq"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) means :: RSSPACE:def 6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) it ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"Zeroseq"::: RSSPACE:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_rsspace :::"Zeroseq"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "b1")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); theorem :: RSSPACE:1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set (Var "x")))) ; theorem :: RSSPACE:2 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "w")) ")" )))) ; theorem :: RSSPACE:3 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ))))) ; registration cluster (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) -> ($#v2_rlvect_1 :::"Abelian"::: ) ; end; theorem :: RSSPACE:4 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )))) ; theorem :: RSSPACE:5 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ; theorem :: RSSPACE:6 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "st" (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ))))) ; theorem :: RSSPACE:7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ))))) ; theorem :: RSSPACE:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))) ; theorem :: RSSPACE:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))) ; theorem :: RSSPACE:10 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ) "holds" (Bool (Set (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ; definitionfunc :::"Linear_Space_of_RealSequences"::: -> ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: RSSPACE:def 7 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" ); end; :: deftheorem defines :::"Linear_Space_of_RealSequences"::: RSSPACE:def 7 : (Bool (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) ) "," (Set ($#k6_rsspace :::"Zeroseq"::: ) ) "," (Set ($#k4_rsspace :::"l_add"::: ) ) "," (Set ($#k5_rsspace :::"l_mult"::: ) ) "#)" )); registration cluster (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ; end; registration cluster (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; definitionlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "X1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume (Bool "(" (Bool (Set (Const "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Const "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ; func :::"Add_"::: "(" "X1" "," "X" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" "X1" equals :: RSSPACE:def 8 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "X") ($#k1_realset1 :::"||"::: ) "X1"); end; :: deftheorem defines :::"Add_"::: RSSPACE:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k8_rsspace :::"Add_"::: ) "(" (Set (Var "X1")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "X"))) ($#k1_realset1 :::"||"::: ) (Set (Var "X1")))))); definitionlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "X1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume (Bool "(" (Bool (Set (Const "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Const "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ; func :::"Mult_"::: "(" "X1" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "X1" equals :: RSSPACE:def 9 (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "X") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," "X1" ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"Mult_"::: RSSPACE:def 9 : (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k9_rsspace :::"Mult_"::: ) "(" (Set (Var "X1")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "X"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "X1")) ($#k2_zfmisc_1 :::":]"::: ) ))))); definitionlet "X" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "X1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume (Bool "(" (Bool (Set (Const "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Const "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ; func :::"Zero_"::: "(" "X1" "," "X" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "X1" equals :: RSSPACE:def 10 (Set ($#k4_struct_0 :::"0."::: ) "X"); end; :: deftheorem defines :::"Zero_"::: RSSPACE:def 10 : (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "X1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k10_rsspace :::"Zero_"::: ) "(" (Set (Var "X1")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))); theorem :: RSSPACE:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) & (Bool (Bool "not" (Set (Var "V1")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set (Var "V1")) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set (Var "V1")) "," (Set (Var "V")) ")" ")" ) "#)" ) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V"))))) ; definitionfunc :::"the_set_of_l2RealSequences"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) means :: RSSPACE:def 11 (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")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" )) "is" ($#v1_series_1 :::"summable"::: ) ) ")" ) ")" )); end; :: deftheorem defines :::"the_set_of_l2RealSequences"::: RSSPACE:def 11 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "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")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" )) "is" ($#v1_series_1 :::"summable"::: ) ) ")" ) ")" )) ")" )); registration cluster (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rlsub_1 :::"linearly-closed"::: ) ; end; theorem :: RSSPACE:12 (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "#)" ) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) )) ; theorem :: RSSPACE:13 (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "#)" ) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::)) ; theorem :: RSSPACE:14 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rsspace :::"the_set_of_RealSequences"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Real_Sequence":::)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")))) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds" (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" ) ($#k1_series_1 :::"+"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "v")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "u")) ")" )))) ")" ) ")" ) ; definitionfunc :::"l_scalar"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: RSSPACE:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "y")) ")" ) ")" )))); end; :: deftheorem defines :::"l_scalar"::: RSSPACE:def 12 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k12_rsspace :::"l_scalar"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "x")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k2_rsspace :::"seq_id"::: ) (Set (Var "y")) ")" ) ")" )))) ")" )); registration cluster (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k12_rsspace :::"l_scalar"::: ) ) "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionfunc :::"l2_Space"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_bhsp_1 :::"UNITSTR"::: ) equals :: RSSPACE:def 13 (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k12_rsspace :::"l_scalar"::: ) ) "#)" ); end; :: deftheorem defines :::"l2_Space"::: RSSPACE:def 13 : (Bool (Set ($#k13_rsspace :::"l2_Space"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set ($#k11_rsspace :::"the_set_of_l2RealSequences"::: ) ) "," (Set ($#k7_rsspace :::"Linear_Space_of_RealSequences"::: ) ) ")" ")" ) "," (Set ($#k12_rsspace :::"l_scalar"::: ) ) "#)" )); theorem :: RSSPACE:15 (Bool "for" (Set (Var "l")) "being" ($#l1_rlvect_1 :::"RLSStruct"::: ) "st" (Bool (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "l"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "l"))) "#)" ) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))) "holds" (Bool (Set (Var "l")) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))) ; theorem :: RSSPACE:16 (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 (Var "rseq")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: RSSPACE:17 (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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "rseq")) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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"::: ) )))) ; registration cluster (Set ($#k13_rsspace :::"l2_Space"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end;