:: EUCLID_7 semantic presentation begin theorem :: EUCLID_7:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "g")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )))) ; theorem :: EUCLID_7:2 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R")))))) ; theorem :: EUCLID_7:3 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "z")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "z")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: EUCLID_7:4 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: EUCLID_7:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k8_euclid :::"-"::: ) (Set (Var "b")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "c")) ")" ) ($#k7_euclid :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_euclid :::"+"::: ) (Set (Var "c")))))) ; registrationlet "f1", "f2" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "f1" "," "f2" ($#k13_funct_3 :::":>"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"<:"::: redefine func :::"<:":::"f1" "," "f2":::":>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "D" "," "D" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "h" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); redefine attr "h" is :::"increasing"::: means :: EUCLID_7:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "h"))) "holds" (Bool (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set "h" ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"increasing"::: EUCLID_7:def 1 : (Bool "for" (Set (Var "h")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); theorem :: EUCLID_7:6 (Bool "for" (Set (Var "h")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: EUCLID_7:7 (Bool "for" (Set (Var "h")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: EUCLID_7:8 (Bool "for" (Set (Var "h")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: EUCLID_7:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rlvect_1 :::"strict"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_rlvect_1 :::"strict"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "V"))))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "h" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Const "F")) ")" ); func "F" :::"(*)"::: "h" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" equals :: EUCLID_7:def 2 (Set "F" ($#k1_partfun1 :::"*"::: ) "h"); end; :: deftheorem defines :::"(*)"::: EUCLID_7:def 2 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k2_euclid_7 :::"(*)"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h"))))))); theorem :: EUCLID_7:10 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )))) ; theorem :: EUCLID_7:11 (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: EUCLID_7:12 (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ; theorem :: EUCLID_7:13 (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool (Set ($#k6_rfinseq2 :::"sort_a"::: ) (Set (Var "h"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )) ; theorem :: EUCLID_7:14 (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "h3")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h")) ")" )(Bool "ex" (Set (Var "h2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "h2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h3")))) & (Bool (Set (Var "h2")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "h2")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h2")))) ")" )))) ; begin definitionlet "B0" be ($#m1_hidden :::"set"::: ) ; attr "B0" is :::"R-orthogonal"::: means :: EUCLID_7:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "B0") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "B0") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"R-orthogonal"::: EUCLID_7:def 3 : (Bool "for" (Set (Var "B0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B0"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B0"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_euclid_7 :::"R-orthogonal"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: EUCLID_7:15 (Bool "for" (Set (Var "B0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B0"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B0"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )) ")" )) ; definitionlet "B0" be ($#m1_hidden :::"set"::: ) ; attr "B0" is :::"R-normal"::: means :: EUCLID_7:def 4 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "B0")) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))); end; :: deftheorem defines :::"R-normal"::: EUCLID_7:def 4 : (Bool "for" (Set (Var "B0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v2_euclid_7 :::"R-normal"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B0")))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_euclid_7 :::"R-normal"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v2_euclid_7 :::"R-normal"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "B0", "B1" be ($#v2_euclid_7 :::"R-normal"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "B0" ($#k2_xboole_0 :::"\/"::: ) "B1") -> ($#v2_euclid_7 :::"R-normal"::: ) ; end; theorem :: EUCLID_7:16 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#v2_euclid_7 :::"R-normal"::: ) )) ; theorem :: EUCLID_7:17 (Bool "for" (Set (Var "B0")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x0")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "B0")) "is" ($#v2_euclid_7 :::"R-normal"::: ) ) & (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x0")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "B0")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )) "is" ($#v2_euclid_7 :::"R-normal"::: ) ))) ; definitionlet "B0" be ($#m1_hidden :::"set"::: ) ; attr "B0" is :::"R-orthonormal"::: means :: EUCLID_7:def 5 (Bool "(" (Bool "B0" "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) & (Bool "B0" "is" ($#v2_euclid_7 :::"R-normal"::: ) ) ")" ); end; :: deftheorem defines :::"R-orthonormal"::: EUCLID_7:def 5 : (Bool "for" (Set (Var "B0")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v3_euclid_7 :::"R-orthonormal"::: ) ) "iff" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) & (Bool (Set (Var "B0")) "is" ($#v2_euclid_7 :::"R-normal"::: ) ) ")" ) ")" )); registration cluster ($#v3_euclid_7 :::"R-orthonormal"::: ) -> ($#v1_euclid_7 :::"R-orthogonal"::: ) ($#v2_euclid_7 :::"R-normal"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_euclid_7 :::"R-orthogonal"::: ) ($#v2_euclid_7 :::"R-normal"::: ) -> ($#v3_euclid_7 :::"R-orthonormal"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v3_euclid_7 :::"R-orthonormal"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_euclid_7 :::"R-orthonormal"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v4_funct_1 :::"functional"::: ) ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#v3_euclid_7 :::"R-orthonormal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "B0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "B0" is :::"complete"::: means :: EUCLID_7:def 6 (Bool "for" (Set (Var "B")) "being" ($#v3_euclid_7 :::"R-orthonormal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) "st" (Bool (Bool "B0" ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) "B0")); end; :: deftheorem defines :::"complete"::: EUCLID_7:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v4_euclid_7 :::"complete"::: ) ) "iff" (Bool "for" (Set (Var "B")) "being" ($#v3_euclid_7 :::"R-orthonormal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B0")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B0")))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "B0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "B0" is :::"orthogonal_basis"::: means :: EUCLID_7:def 7 (Bool "(" (Bool "B0" "is" ($#v3_euclid_7 :::"R-orthonormal"::: ) ) & (Bool "B0" "is" ($#v4_euclid_7 :::"complete"::: ) ) ")" ); end; :: deftheorem defines :::"orthogonal_basis"::: EUCLID_7:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v5_euclid_7 :::"orthogonal_basis"::: ) ) "iff" (Bool "(" (Bool (Set (Var "B0")) "is" ($#v3_euclid_7 :::"R-orthonormal"::: ) ) & (Bool (Set (Var "B0")) "is" ($#v4_euclid_7 :::"complete"::: ) ) ")" ) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v5_euclid_7 :::"orthogonal_basis"::: ) -> ($#v3_euclid_7 :::"R-orthonormal"::: ) ($#v4_euclid_7 :::"complete"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )); cluster ($#v3_euclid_7 :::"R-orthonormal"::: ) ($#v4_euclid_7 :::"complete"::: ) -> ($#v5_euclid_7 :::"orthogonal_basis"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )); end; theorem :: EUCLID_7:18 (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "B0")) "is" ($#v5_euclid_7 :::"orthogonal_basis"::: ) )) "holds" (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: EUCLID_7:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "B0")) "is" ($#v5_euclid_7 :::"orthogonal_basis"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B0")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); attr "X" is :::"linear_manifold"::: means :: EUCLID_7:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) "X"))); end; :: deftheorem defines :::"linear_manifold"::: EUCLID_7:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_euclid_7 :::"linear_manifold"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_subset_1 :::"[#]"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )) -> ($#v6_euclid_7 :::"linear_manifold"::: ) ; end; theorem :: EUCLID_7:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v6_euclid_7 :::"linear_manifold"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) "n" ")" ) ($#k1_tarski :::"}"::: ) ) -> ($#v6_euclid_7 :::"linear_manifold"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); func :::"L_Span"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLID_7:def 9 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) : (Bool "(" (Bool (Set (Var "Y")) "is" ($#v6_euclid_7 :::"linear_manifold"::: ) ) & (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) "}" ); end; :: deftheorem defines :::"L_Span"::: EUCLID_7:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k3_euclid_7 :::"L_Span"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Var "n")) ")" ) : (Bool "(" (Bool (Set (Var "Y")) "is" ($#v6_euclid_7 :::"linear_manifold"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ) "}" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k3_euclid_7 :::"L_Span"::: ) "X") -> ($#v6_euclid_7 :::"linear_manifold"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"accum"::: "f" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") means :: EUCLID_7:def 10 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it)) & (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"accum"::: EUCLID_7:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_7 :::"accum"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"Sum"::: "f" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") equals :: EUCLID_7:def 11 (Set (Set "(" ($#k4_euclid_7 :::"accum"::: ) "f" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" )) if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Set ($#k5_euclid :::"0*"::: ) "n"); end; :: deftheorem defines :::"Sum"::: EUCLID_7:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_euclid_7 :::"accum"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" ")" ))); theorem :: EUCLID_7:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "F2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_euclid_7 :::"(*)"::: ) (Set (Var "h"))))) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "F"))))))) ; theorem :: EUCLID_7:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: EUCLID_7:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "F")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")))) & (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 "g")))) & (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "F")))))))) ; theorem :: EUCLID_7:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "F")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h")))) & (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 "g")))) & (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "F")))))))) ; begin definitionlet "n", "i" be ($#m1_hidden :::"Nat":::); :: original: :::"Base_FinSeq"::: redefine func :::"Base_FinSeq"::: "(" "n" "," "i" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n"); end; theorem :: EUCLID_7:25 (Bool "for" (Set (Var "n")) "," (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i2")) ")" ))) "holds" (Bool (Set (Var "i1")) ($#r1_hidden :::"="::: ) (Set (Var "i2")))) ; theorem :: EUCLID_7:26 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k11_euclid :::"sqr"::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ))) ; theorem :: EUCLID_7:27 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: EUCLID_7:28 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: EUCLID_7:29 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "j")) ")" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: EUCLID_7:30 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x0" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Const "n"))); func :::"ProjFinSeq"::: "x0" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) "n") means :: EUCLID_7:def 12 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) "n") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) "x0" "," (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" "n" "," (Set (Var "i")) ")" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_euclid :::"*"::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" "n" "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"ProjFinSeq"::: EUCLID_7:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_euclid_7 :::"ProjFinSeq"::: ) (Set (Var "x0")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x0")) "," (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_euclid :::"*"::: ) (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ) ")" )))); theorem :: EUCLID_7:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid_7 :::"Sum"::: ) (Set "(" ($#k7_euclid_7 :::"ProjFinSeq"::: ) (Set (Var "x0")) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"RN_Base"::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ) equals :: EUCLID_7:def 13 "{" (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" "n" "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n") ")" ) "}" ; end; :: deftheorem defines :::"RN_Base"::: EUCLID_7:def 13 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_euclid_7 :::"Base_FinSeq"::: ) "(" (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "}" )); theorem :: EUCLID_7:32 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registration cluster (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k8_euclid_7 :::"RN_Base"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k8_euclid_7 :::"RN_Base"::: ) "n") -> ($#v5_euclid_7 :::"orthogonal_basis"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v4_funct_1 :::"functional"::: ) ($#v3_finseq_1 :::"FinSequence-membered"::: ) ($#v5_euclid_7 :::"orthogonal_basis"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); mode Orthogonal_Basis of "n" is ($#v5_euclid_7 :::"orthogonal_basis"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" ); end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster ($#v5_euclid_7 :::"orthogonal_basis"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_euclid :::"REAL"::: ) "n" ")" )); end; begin registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k7_real_ns1 :::"REAL-US"::: ) "n") -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) "n" ")" )); end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Const "n")) ")" ); let "a", "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Const "n")) ")" ); let "y" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); identify ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Const "n")) ")" ); let "a" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Const "n")) ")" ); let "a", "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; theorem :: EUCLID_7:33 (Bool "for" (Set (Var "n")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" )) (Bool "for" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "v0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "Bn")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "Bn")) "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "l")))) & (Bool (Set (Var "v0")) ($#r2_hidden :::"in"::: ) (Set (Var "Bn"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "l")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "v0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v0")) "," (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "l")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v0")) "," (Set "(" (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v0")) ")" ) ")" ))))))) ; theorem :: EUCLID_7:34 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g"))))))) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k10_funcsdom :::"RealVectSpace"::: ) "A") -> ($#v1_monoid_0 :::"constituted-Functions"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" )) -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) "A" ")" )); end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set (Const "A")) ")" ); let "a", "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set (Const "A")) ")" ); let "y" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); identify ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set (Const "A")) ")" ); let "a" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "x", "y" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set (Const "A")) ")" ); let "a", "b" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); identify ; end; theorem :: EUCLID_7:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))))) ; theorem :: EUCLID_7:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "x")) ($#k7_euclid :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))))) ; theorem :: EUCLID_7:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_euclid :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_euclid :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))))) ; theorem :: EUCLID_7:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: EUCLID_7:39 (Bool "for" (Set (Var "n")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" )) (Bool "for" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) (Bool "for" (Set (Var "v0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "Bn")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "Bn")) "is" ($#v1_euclid_7 :::"R-orthogonal"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "l")))) & (Bool (Set (Var "v0")) ($#r2_hidden :::"in"::: ) (Set (Var "Bn"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "l")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Var "v0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v0")) "," (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "l")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_real_ns1 :::"Euclid_scalar"::: ) (Set (Var "n")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v0")) "," (Set "(" (Set "(" (Set (Var "l")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v0")) ")" ) ")" ))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v3_euclid_7 :::"R-orthonormal"::: ) -> ($#v1_rlvect_3 :::"linearly-independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) ")" ))); end; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#v3_euclid_7 :::"R-orthonormal"::: ) -> ($#v1_rlvect_3 :::"linearly-independent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) "n" ")" ))); end; theorem :: EUCLID_7:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Bn")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "Bn")) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Bn"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Bn"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_euclid :::"*"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; begin registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k8_euclid_7 :::"RN_Base"::: ) "n") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: EUCLID_7:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: EUCLID_7:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k5_euclid_7 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g"))))))) ; theorem :: EUCLID_7:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "B")) "st" (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l")))))))) ; theorem :: EUCLID_7:44 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "B")) "st" (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l")))))))) ; theorem :: EUCLID_7:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "B")) "is" ($#m1_rlvect_3 :::"Basis"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" )) -> ($#v1_rlvect_5 :::"finite-dimensional"::: ) ; end; theorem :: EUCLID_7:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_rlvect_5 :::"dim"::: ) (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: EUCLID_7:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_rlvect_3 :::"Basis"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: EUCLID_7:48 (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_rlvect_3 :::"Basis"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) ; theorem :: EUCLID_7:49 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k8_euclid_7 :::"RN_Base"::: ) (Set (Var "n"))) "is" ($#m1_rusub_3 :::"Basis"::: ) "of" (Set ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n"))))) ; theorem :: EUCLID_7:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Orthogonal_Basis":::) "of" (Set (Var "n")) "holds" (Bool (Set (Var "D")) "is" ($#m1_rlvect_3 :::"Basis"::: ) "of" (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ))))) ; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k7_real_ns1 :::"REAL-US"::: ) "n") -> ($#v1_rusub_4 :::"finite-dimensional"::: ) ; end; theorem :: EUCLID_7:51 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set "(" ($#k7_real_ns1 :::"REAL-US"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: EUCLID_7:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Orthogonal_Basis":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ;