:: BHSP_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"UNITSTR"::: -> ($#l1_rlvect_1 :::"RLSStruct"::: ) ; aggr :::"UNITSTR":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult":::, :::"scalar"::: #) -> ($#l1_bhsp_1 :::"UNITSTR"::: ) ; sel :::"scalar"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_bhsp_1 :::"strict"::: ) for ($#l1_bhsp_1 :::"UNITSTR"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "a" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "m" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D")); let "s" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" "D" "," "Z" "," "a" "," "m" "," "s" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_bhsp_1 :::"UNITSTR"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func "x" :::".|."::: "y" -> ($#m1_subset_1 :::"Real":::) equals :: BHSP_1:def 1 (Set (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" "X") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) "x" "," "y" ($#k1_domain_1 :::"]"::: ) )); end; :: deftheorem defines :::".|."::: BHSP_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_bhsp_1 :::"UNITSTR"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" (Set (Var "X"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_bhsp_1 :::"UNITSTR"::: ) ; attr "IT" is :::"RealUnitarySpace-like"::: means :: BHSP_1:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" "IT" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "implies" (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))) ")" ))); end; :: deftheorem defines :::"RealUnitarySpace-like"::: BHSP_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_bhsp_1 :::"UNITSTR"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "implies" (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))) ")" ))) ")" )); registration cluster ($#~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"::: ) ($#v1_bhsp_1 :::"strict"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) for ($#l1_bhsp_1 :::"UNITSTR"::: ) ; end; definitionmode RealUnitarySpace is ($#~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"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) ; end; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); :: original: :::".|."::: redefine func "x" :::".|."::: "y" -> ($#m1_subset_1 :::"Real":::); commutativity (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "x"))))) ; end; theorem :: BHSP_1:1 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: BHSP_1:2 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ))))) ; theorem :: BHSP_1:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" )))))) ; theorem :: BHSP_1:4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )))))) ; theorem :: BHSP_1:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ")" )))))) ; theorem :: BHSP_1:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ")" )))))) ; theorem :: BHSP_1:7 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:8 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:9 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:10 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")))))) ; theorem :: BHSP_1:11 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ))))) ; theorem :: BHSP_1:12 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "z")) ")" ))))) ; theorem :: BHSP_1:13 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "u")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "v")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "u")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "v")) ")" ))))) ; theorem :: BHSP_1:14 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BHSP_1:15 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BHSP_1:16 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:17 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:18 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:19 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ) ")" ))))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); pred "x" "," "y" :::"are_orthogonal"::: means :: BHSP_1:def 3 (Bool (Set "x" ($#k2_bhsp_1 :::".|."::: ) "y") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); symmetry (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; end; :: deftheorem defines :::"are_orthogonal"::: BHSP_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) ) "iff" (Bool (Set (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); theorem :: BHSP_1:20 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Var "x")) "," (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_bhsp_1 :::"are_orthogonal"::: ) ))) ; theorem :: BHSP_1:21 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) ))) ; theorem :: BHSP_1:22 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) "," (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_bhsp_1 :::"are_orthogonal"::: ) ))) ; theorem :: BHSP_1:23 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) "," (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r1_bhsp_1 :::"are_orthogonal"::: ) ))) ; theorem :: BHSP_1:24 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; theorem :: BHSP_1:25 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_bhsp_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" ))))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"||.":::"x":::".||"::: -> ($#m1_subset_1 :::"Real":::) equals :: BHSP_1:def 4 (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" "x" ($#k2_bhsp_1 :::".|."::: ) "x" ")" )); end; :: deftheorem defines :::"||."::: BHSP_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "x")) ")" ))))); theorem :: BHSP_1:26 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ))) ; theorem :: BHSP_1:27 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )))))) ; theorem :: BHSP_1:28 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )))) ; theorem :: BHSP_1:29 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k2_bhsp_1 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ))))) ; theorem :: BHSP_1:30 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ))))) ; theorem :: BHSP_1:31 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )))) ; theorem :: BHSP_1:32 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )))) ; theorem :: BHSP_1:33 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"dist"::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Real":::) equals :: BHSP_1:def 5 (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" "x" ($#k5_algstr_0 :::"-"::: ) "y" ")" ) ($#k3_bhsp_1 :::".||"::: ) ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )))) ; end; :: deftheorem defines :::"dist"::: BHSP_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )))); theorem :: BHSP_1:34 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BHSP_1:35 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" ))))) ; theorem :: BHSP_1:36 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: BHSP_1:37 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BHSP_1:38 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: BHSP_1:39 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k2_bhsp_1 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ))))) ; theorem :: BHSP_1:40 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "u")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: BHSP_1:41 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "u")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "y")) "," (Set (Var "v")) ")" ")" ))))) ; theorem :: BHSP_1:42 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: BHSP_1:43 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_bhsp_1 :::"dist"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) "," (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "z")) "," (Set (Var "x")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_bhsp_1 :::"dist"::: ) "(" (Set (Var "z")) "," (Set (Var "y")) ")" ")" ))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func "seq" :::"+"::: "x" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: BHSP_1:def 6 (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 "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) "x"))); end; :: deftheorem defines :::"+"::: BHSP_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x"))))) ")" ))))); theorem :: BHSP_1:44 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq1", "seq2" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"+"::: redefine func "seq1" :::"+"::: "seq2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#k2_zfmisc_1 :::":]"::: ) )); commutativity (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq2")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq1"))))) ; end; theorem :: BHSP_1:45 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq3")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq3")))))) ; theorem :: BHSP_1:46 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v3_funct_1 :::"constant"::: ) ))) ; theorem :: BHSP_1:47 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v3_funct_1 :::"constant"::: ) ))) ; theorem :: BHSP_1:48 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq1"))) "is" ($#v3_funct_1 :::"constant"::: ) )))) ; theorem :: BHSP_1:49 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: BHSP_1:50 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "seq")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ))))) ; theorem :: BHSP_1:51 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq2")) ")" )))))) ; theorem :: BHSP_1:52 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_1:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_1:54 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Num 1) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Var "seq"))))) ; theorem :: BHSP_1:55 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")))))) ; theorem :: BHSP_1:56 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq")) ($#k5_bhsp_1 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )))))) ; theorem :: BHSP_1:57 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq1")) ")" ))))) ; theorem :: BHSP_1:58 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "seq")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq")) ($#k4_normsp_1 :::"-"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ))))) ; theorem :: BHSP_1:59 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "seq")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" ))))) ; theorem :: BHSP_1:60 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq3")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq3")))))) ; theorem :: BHSP_1:61 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq3"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq3")) ")" ))))) ; theorem :: BHSP_1:62 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq3")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq3")))))) ; theorem :: BHSP_1:63 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq2")) ")" )))))) ;