:: BHSP_5  semantic presentation begin  

















theorem :: BHSP_5:1 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "p1")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "p2")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p2"))))) "holds"  (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p2")))) & (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p1")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p1"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p1")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p1"))))  ")" ))  ")" ))) ; 
 definitionlet "DX" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "DX")); assume that  
(Bool  "("  (Bool (Set (Const "f")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Const "f")) "is"   ($#v2_binop_1 :::"associative"::: )  )  ")" )
 and  
(Bool (Set (Const "f")) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )
 ; let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "DX")); func "f" :::"++"::: "Y" ->    ($#m1_subset_1 :::"Element"::: )   "of" "DX" means :: BHSP_5:def 1 (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "DX" "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "Y") & (Bool it  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p"))))  ")" )); end; 








:: deftheorem    defines :::"++"::: BHSP_5:def 1 :  (Bool  "for" (Set (Var "DX")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "DX"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX"))  (Bool  "for" (Set (Var "b4")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "DX")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_bhsp_5 :::"++"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "DX")) "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p"))))  ")" ))  ")" ))))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func  :::"setop_SUM":::  "(" "Y" "," "X" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: BHSP_5:def 2 (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "X")  ($#k1_bhsp_5 :::"++"::: )  "Y") if (Bool "Y"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Set   ($#k4_struct_0 :::"0."::: )  "X"); end; 






:: deftheorem    defines :::"setop_SUM"::: BHSP_5:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set   ($#k2_bhsp_5 :::"setop_SUM"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_bhsp_5 :::"++"::: )  (Set (Var "Y"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool (Set   ($#k2_bhsp_5 :::"setop_SUM"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X"))))  ")"   ")" ))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "p" be   ($#m1_hidden :::"FinSequence":::); let "i" be   ($#m1_hidden :::"Nat":::); func  :::"PO":::  "(" "i" "," "p" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: BHSP_5:def 3 (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" "X")  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) "x" "," (Set  "(" "p"  ($#k1_funct_1 :::"."::: )  "i" ")" ) ($#k4_tarski :::"]"::: ) )); end; 








:: deftheorem    defines :::"PO"::: BHSP_5:def 3 :  (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 "p")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_bhsp_5 :::"PO"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ))))))); 
 definitionlet "DK", "DX" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "DX")) "," (Set (Const "DK")); let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "DX")); func  :::"Func_Seq":::  "(" "F" "," "p" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "DK" equals :: BHSP_5:def 4 (Set "F"  ($#k3_relat_1 :::"*"::: )  "p"); end; 








:: deftheorem    defines :::"Func_Seq"::: BHSP_5:def 4 :  (Bool  "for" (Set (Var "DK")) "," (Set (Var "DX")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set (Var "DK"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "DX")) "holds"  (Bool (Set   ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "F")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "p"))))))); 
 definitionlet "DK", "DX" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "DK")); assume that  
(Bool  "("  (Bool (Set (Const "f")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Const "f")) "is"   ($#v2_binop_1 :::"associative"::: )  )  ")" )
 and  
(Bool (Set (Const "f")) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )
 ; let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "DX")); let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "DX")) "," (Set (Const "DK")); assume 
(Bool (Set (Const "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "F"))))
 ; func  :::"setopfunc":::  "(" "Y" "," "DX" "," "DK" "," "F" "," "f" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "DK" means :: BHSP_5:def 5 (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "DX" "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "Y") & (Bool it  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" "F" "," (Set (Var "p")) ")"  ")" )))  ")" )); end; 










:: deftheorem    defines :::"setopfunc"::: BHSP_5:def 5 :  (Bool  "for" (Set (Var "DK")) "," (Set (Var "DX")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "DK"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set (Var "DK"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "b6")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "DK")) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "DX")) "," (Set (Var "DK")) "," (Set (Var "F")) "," (Set (Var "f")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "DX")) "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "F")) "," (Set (Var "p")) ")"  ")" )))  ")" ))  ")" )))))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func  :::"setop_xPre_PROD":::  "(" "x" "," "Y" "," "X" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: BHSP_5:def 6 (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "Y") & (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_bhsp_5 :::"PO"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) "," "x" ")" ))  ")" ) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set (Var "q"))))  ")" ))  ")" )); end; 







:: deftheorem    defines :::"setop_xPre_PROD"::: BHSP_5:def 6 :  (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 "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_bhsp_5 :::"setop_xPre_PROD"::: )   "(" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "X")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_bhsp_5 :::"PO"::: )   "(" (Set (Var "i")) "," (Set (Var "p")) "," (Set (Var "x")) ")" ))  ")" ) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set (Var "q"))))  ")" ))  ")" ))  ")" ))))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func  :::"setop_xPROD":::  "(" "x" "," "Y" "," "X" ")"  ->   ($#m1_subset_1 :::"Real":::) equals :: BHSP_5:def 7 (Set   ($#k6_bhsp_5 :::"setop_xPre_PROD"::: )   "(" "x" "," "Y" "," "X" ")" ) if (Bool "Y"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Set   ($#k6_numbers :::"0"::: )  ); end; 







:: deftheorem    defines :::"setop_xPROD"::: BHSP_5:def 7 :  (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 "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set   ($#k7_bhsp_5 :::"setop_xPROD"::: )   "(" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_bhsp_5 :::"setop_xPre_PROD"::: )   "(" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "X")) ")" ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool (Set   ($#k7_bhsp_5 :::"setop_xPROD"::: )   "(" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )))); 
 begin  definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); mode  :::"OrthogonalFamily":::  "of" "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BHSP_5:def 8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))); end; 





:: deftheorem    defines :::"OrthogonalFamily"::: BHSP_5:def 8 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" ))); 
 
theorem :: BHSP_5:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X")))) ; 
 registrationlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); 
cluster   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" "X"; 
end; definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); mode  :::"OrthonormalFamily":::  "of" "X" ->   ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BHSP_5:def 9 (Bool  "("  (Bool it "is"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" "X") & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")" ); end; 





:: deftheorem    defines :::"OrthonormalFamily"::: BHSP_5:def 9 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")" )  ")" ))); 
 
theorem :: BHSP_5:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X")))) ; 
 registrationlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); 
cluster   ($#v1_finset_1 :::"finite"::: )    for    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" "X"; 
end; 
theorem :: BHSP_5: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  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" ))) ; 
 begin  
theorem :: BHSP_5: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 (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Num 2)  ($#k11_binop_2 :::"*"::: )  (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))))) ; 
 
theorem :: BHSP_5:6 (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  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "y")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_binop_2 :::"+"::: )  (Set  "(" (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "y")) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  ")" ))))) ; 
 
theorem :: BHSP_5:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")) ")" ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )) "holds"  (Bool (Set (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p")) ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set (Var "q"))))))) ; 
 
theorem :: BHSP_5:8 (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 "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set (Var "q")))))))) ; 
 
theorem :: BHSP_5:9 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y1"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "y2"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y2")))) "holds"  (Bool (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y2")) ")" ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "F")) "," (Set (Var "p")) ")"  ")" ) ")" ) "," (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "F")) "," (Set (Var "p")) ")"  ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "H")) "," (Set (Var "p")) ")"  ")" )))))))) ; 
 
theorem :: BHSP_5:10 (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 "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set  "the"  ($#u1_bhsp_1 :::"scalar"::: )  "of" (Set (Var "X")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "F")) "," (Set (Var "p")) ")"  ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set  "("  ($#k4_bhsp_5 :::"Func_Seq"::: )   "(" (Set (Var "H")) "," (Set (Var "p")) ")"  ")" ))))))))) ; 
 
theorem :: BHSP_5:11 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y"))))  ")" )) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "F")) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "H")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))))) ; 
 
theorem :: BHSP_5:12 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y"))))  ")" )) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "F")) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) ")"  ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "F")) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "H")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))))) ; 
 
theorem :: BHSP_5:13 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y")) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )) "holds"  (Bool (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "H")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )  ($#k5_square_1 :::"^2"::: )  )))))) ; 
 
theorem :: BHSP_5:14 (Bool  "for" (Set (Var "DK")) "," (Set (Var "DX")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "DK"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX"))  "st" (Bool (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y2")))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set (Var "DK"))  "st" (Bool (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "Y2"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX"))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y2"))))) "holds"  (Bool (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Z")) "," (Set (Var "DX")) "," (Set (Var "DK")) "," (Set (Var "F")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_binop_1 :::"."::: )   "(" (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y1")) "," (Set (Var "DX")) "," (Set (Var "DK")) "," (Set (Var "F")) "," (Set (Var "f")) ")"  ")" ) "," (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y2")) "," (Set (Var "DX")) "," (Set (Var "DK")) "," (Set (Var "F")) "," (Set (Var "f")) ")"  ")" ) ")" ))))))) ;