:: PRVECT_2 semantic presentation begin theorem :: PRVECT_2:1 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "t")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "g")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool "(" (Bool (Set (Var "t")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_2:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (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 ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "y")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "y")) ($#k12_euclid :::".|"::: ) ))) ; theorem :: PRVECT_2:3 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (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 "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; mode :::"MultOps"::: "of" "X" "," "f" -> ($#m1_hidden :::"Function":::) means :: PRVECT_2:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"MultOps"::: PRVECT_2:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set (Var "X")) "," (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" )))); registrationlet "F" be ($#m1_hidden :::"Domain-Sequence":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_prvect_2 :::"MultOps"::: ) "of" "X" "," "F"; end; theorem :: PRVECT_2:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set (Var "X")) "," (Set (Var "F"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" )))) ; definitionlet "F" be ($#m1_hidden :::"Domain-Sequence":::); let "X" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set (Const "X")) "," (Set (Const "F")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "F"))); :: original: :::"."::: redefine func "p" :::"."::: "i" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) "i" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) "i" ")" ); end; theorem :: PRVECT_2:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "F")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "F"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")))))) ")" )) "holds" (Bool (Set (Var "f")) ($#r8_binop_1 :::"="::: ) (Set (Var "g")))))) ; definitionlet "F" be ($#m1_hidden :::"Domain-Sequence":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set (Const "X")) "," (Set (Const "F")); func :::"[:":::"p":::":]"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" ($#k4_card_3 :::"product"::: ) "F" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) "F" ")" ) means :: PRVECT_2:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) "F") (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "F") "holds" (Bool (Set (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "d")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))))); end; :: deftheorem defines :::"[:"::: PRVECT_2:def 2 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set (Var "X")) "," (Set (Var "F")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "F")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "F")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_prvect_2 :::"[:"::: ) (Set (Var "p")) ($#k2_prvect_2 :::":]"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "F"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) "holds" (Bool (Set (Set "(" (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "d")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "d")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))))) ")" ))))); definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"RealLinearSpace-yielding"::: means :: PRVECT_2:def 3 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "S")) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))); end; :: deftheorem defines :::"RealLinearSpace-yielding"::: PRVECT_2:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "S")) "is" ($#l1_rlvect_1 :::"RealLinearSpace":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode RealLinearSpace-Sequence is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ($#m1_hidden :::"FinSequence":::); end; definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); let "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); :: original: :::"."::: redefine func "G" :::"."::: "j" -> ($#l1_rlvect_1 :::"RealLinearSpace":::); end; definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); func :::"carr"::: "G" -> ($#m1_hidden :::"Domain-Sequence":::) means :: PRVECT_2:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "G")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "G") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "G" ($#k3_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"carr"::: PRVECT_2:def 4 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Domain-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "G")) ($#k3_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); let "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Const "G")) ")" )); :: original: :::"."::: redefine func "G" :::"."::: "j" -> ($#l1_rlvect_1 :::"RealLinearSpace":::); end; definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); func :::"addop"::: "G" -> ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set ($#k4_prvect_2 :::"carr"::: ) "G") means :: PRVECT_2:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k9_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" "G" ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); func :::"complop"::: "G" -> ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set ($#k4_prvect_2 :::"carr"::: ) "G") means :: PRVECT_2:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k10_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set "(" "G" ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); func :::"zeros"::: "G" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) means :: PRVECT_2:def 7 (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k8_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" "G" ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" )))); func :::"multop"::: "G" -> ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k4_prvect_2 :::"carr"::: ) "G") means :: PRVECT_2:def 8 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k1_prvect_2 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" "G" ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"addop"::: PRVECT_2:def 5 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_prvect_2 :::"addop"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k9_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" (Set (Var "G")) ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"complop"::: PRVECT_2:def 6 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_prvect_2 :::"complop"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k10_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set "(" (Set (Var "G")) ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"zeros"::: PRVECT_2:def 7 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_prvect_2 :::"zeros"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k8_prvect_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" (Set (Var "G")) ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" )))) ")" ))); :: deftheorem defines :::"multop"::: PRVECT_2:def 8 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_prvect_2 :::"MultOps"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_prvect_2 :::"multop"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k1_prvect_2 :::"."::: ) (Set (Var "j"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" (Set (Var "G")) ($#k5_prvect_2 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); func :::"product"::: "G" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: PRVECT_2:def 9 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" ) ")" ) "," (Set "(" ($#k8_prvect_2 :::"zeros"::: ) "G" ")" ) "," (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k6_prvect_2 :::"addop"::: ) "G" ")" ) ($#k13_prvect_1 :::":]"::: ) ) "," (Set ($#k2_prvect_2 :::"[:"::: ) (Set "(" ($#k9_prvect_2 :::"multop"::: ) "G" ")" ) ($#k2_prvect_2 :::":]"::: ) ) "#)" ); end; :: deftheorem defines :::"product"::: PRVECT_2:def 9 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) "holds" (Bool (Set ($#k10_prvect_2 :::"product"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" ($#k8_prvect_2 :::"zeros"::: ) (Set (Var "G")) ")" ) "," (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k6_prvect_2 :::"addop"::: ) (Set (Var "G")) ")" ) ($#k13_prvect_1 :::":]"::: ) ) "," (Set ($#k2_prvect_2 :::"[:"::: ) (Set "(" ($#k9_prvect_2 :::"multop"::: ) (Set (Var "G")) ")" ) ($#k2_prvect_2 :::":]"::: ) ) "#)" ))); registrationlet "G" be ($#m1_hidden :::"RealLinearSpace-Sequence":::); cluster (Set ($#k10_prvect_2 :::"product"::: ) "G") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; begin definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"RealNormSpace-yielding"::: means :: PRVECT_2:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "x")) "is" ($#l1_normsp_1 :::"RealNormSpace":::))); end; :: deftheorem defines :::"RealNormSpace-yielding"::: PRVECT_2:def 10 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "x")) "is" ($#l1_normsp_1 :::"RealNormSpace":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode RealNormSpace-Sequence is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ($#m1_hidden :::"FinSequence":::); end; definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); let "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "G"))); :: original: :::"."::: redefine func "G" :::"."::: "j" -> ($#l1_normsp_1 :::"RealNormSpace":::); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) -> ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Const "G")) ")" )); func :::"normsequence"::: "(" "G" "," "x" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "G" ")" )) means :: PRVECT_2:def 11 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "G")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "G") "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" (Set "(" "G" ($#k11_prvect_2 :::"."::: ) (Set (Var "j")) ")" )) ($#k1_seq_1 :::"."::: ) (Set "(" "x" ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"normsequence"::: PRVECT_2:def 11 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "j")) ")" )) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); func :::"productnorm"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PRVECT_2:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) "G" ")" )) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" "G" "," (Set (Var "x")) ")" ")" ) ($#k12_euclid :::".|"::: ) ))); end; :: deftheorem defines :::"productnorm"::: PRVECT_2:def 12 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_prvect_2 :::"productnorm"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" ) ($#k12_euclid :::".|"::: ) ))) ")" ))); definitionlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); func :::"product"::: "G" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) means :: PRVECT_2:def 13 (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k10_prvect_2 :::"product"::: ) "G")) & (Bool (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k13_prvect_2 :::"productnorm"::: ) "G")) ")" ); end; :: deftheorem defines :::"product"::: PRVECT_2:def 13 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k10_prvect_2 :::"product"::: ) (Set (Var "G")))) & (Bool (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" (Set (Var "b2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k13_prvect_2 :::"productnorm"::: ) (Set (Var "G")))) ")" ) ")" ))); theorem :: PRVECT_2:6 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) "holds" (Bool (Set ($#k14_prvect_2 :::"product"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" ($#k8_prvect_2 :::"zeros"::: ) (Set (Var "G")) ")" ) "," (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k6_prvect_2 :::"addop"::: ) (Set (Var "G")) ")" ) ($#k13_prvect_1 :::":]"::: ) ) "," (Set ($#k2_prvect_2 :::"[:"::: ) (Set "(" ($#k9_prvect_2 :::"multop"::: ) (Set (Var "G")) ")" ) ($#k2_prvect_2 :::":]"::: ) ) "," (Set "(" ($#k13_prvect_2 :::"productnorm"::: ) (Set (Var "G")) ")" ) "#)" ))) ; theorem :: PRVECT_2:7 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "y")) ")" ")" ) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: PRVECT_2:8 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k6_prvect_2 :::"addop"::: ) (Set (Var "G")) ")" ) ($#k13_prvect_1 :::":]"::: ) ) ($#k12_prvect_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" ) ($#k7_euclid :::"+"::: ) (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "y")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: PRVECT_2:9 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k12_prvect_2 :::"normsequence"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))) ; registrationlet "G" be ($#m1_hidden :::"RealNormSpace-Sequence":::); cluster (Set ($#k14_prvect_2 :::"product"::: ) "G") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v1_normsp_1 :::"strict"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; theorem :: PRVECT_2:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) (Bool "for" (Set (Var "xi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "xi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "xi")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))))))) ; theorem :: PRVECT_2:11 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "xi")) "," (Set (Var "yi")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) (Bool "for" (Set (Var "zx")) "," (Set (Var "zy")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "xi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "zx")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "zx")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "yi")) ($#r1_hidden :::"="::: ) (Set (Set (Var "zy")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "zy")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "yi")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "xi")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))))))) ; theorem :: PRVECT_2:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "y0"))) & (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x0")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "ex" (Set (Var "seqi")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "seqi")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Set (Var "y0")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seqi")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "seqm")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool "(" (Bool (Set (Var "seqm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")))) & (Bool (Set (Set (Var "seqi")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seqm")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ) ")" ))))))) ; theorem :: PRVECT_2:13 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "G")) ")" ) (Bool "for" (Set (Var "y0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "y0"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) (Bool "ex" (Set (Var "seqi")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "seqi")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set (Set (Var "y0")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seqi")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "seqm")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k4_prvect_2 :::"carr"::: ) (Set (Var "G")) ")" )) "st" (Bool "(" (Bool (Set (Var "seqm")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")))) & (Bool (Set (Set (Var "seqi")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seqm")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "x0"))) ")" ))))) ; theorem :: PRVECT_2:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) "holds" (Bool (Set (Set (Var "G")) ($#k11_prvect_2 :::"."::: ) (Set (Var "i"))) "is" ($#v3_lopban_1 :::"complete"::: ) ) ")" )) "holds" (Bool (Set ($#k14_prvect_2 :::"product"::: ) (Set (Var "G"))) "is" ($#v3_lopban_1 :::"complete"::: ) )) ;