:: RVSUM_1 semantic presentation begin registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) bbbadV1_FINSET_1() "n" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Relation":::); :: original: :::"rng"::: redefine func :::"rng"::: "F" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "D")); let "F1" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "F1" ($#k3_relat_1 :::"(#)"::: ) "F") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "r" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "r1", "r2" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "r1" "," "r2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "r1", "r2", "r3" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "r1" "," "r2" "," "r3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "r1", "r2", "r3", "r4" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k7_finseq_4 :::"<*"::: ) "r1" "," "r2" "," "r3" "," "r4" ($#k7_finseq_4 :::"*>"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "j" be ($#m1_hidden :::"Nat":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "j" ($#k2_finseq_2 :::"|->"::: ) "r") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f", "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k7_finseq_1 :::"^"::: ) "g") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; theorem :: RVSUM_1:1 (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ; definitionredefine func :::"diffreal"::: equals :: RVSUM_1:def 1 (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set ($#k31_binop_2 :::"compreal"::: ) ) ")" ); end; :: deftheorem defines :::"diffreal"::: RVSUM_1:def 1 : (Bool (Set ($#k34_binop_2 :::"diffreal"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set ($#k31_binop_2 :::"compreal"::: ) ) ")" )); definitionfunc :::"sqrreal"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RVSUM_1:def 2 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ))); end; :: deftheorem defines :::"sqrreal"::: RVSUM_1:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_rvsum_1 :::"sqrreal"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ))) ")" )); theorem :: RVSUM_1:2 (Bool (Num 1) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k35_binop_2 :::"multreal"::: ) )) ; theorem :: RVSUM_1:3 (Bool (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ; theorem :: RVSUM_1:4 (Bool (Set ($#k2_rvsum_1 :::"sqrreal"::: ) ) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k35_binop_2 :::"multreal"::: ) )) ; definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"multreal"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 3 (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k5_funcop_1 :::"[;]"::: ) "(" "x" "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"multreal"::: RVSUM_1:def 3 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k3_rvsum_1 :::"multreal"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ))); theorem :: RVSUM_1:5 (Bool "for" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k3_rvsum_1 :::"multreal"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r1"))))) ; theorem :: RVSUM_1:6 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k3_rvsum_1 :::"multreal"::: ) ) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) ))) ; theorem :: RVSUM_1:7 (Bool (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ; theorem :: RVSUM_1:8 (Bool (Set ($#k33_binop_2 :::"addreal"::: ) ) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) ; theorem :: RVSUM_1:9 (Bool (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ($#r2_funct_2 :::"="::: ) (Set ($#k31_binop_2 :::"compreal"::: ) )) ; theorem :: RVSUM_1:10 (Bool (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set ($#k33_binop_2 :::"addreal"::: ) )) ; definitionlet "F1", "F2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"+"::: redefine func "F1" :::"+"::: "F2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 4 (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" "F1" "," "F2" ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F2")) "," (Set (Var "F1")) ")" )))) ; end; :: deftheorem defines :::"+"::: RVSUM_1:def 4 : (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); :: original: :::"+"::: redefine func "R1" :::"+"::: "R2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:11 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R2")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "R2")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" )))))) ; theorem :: RVSUM_1:12 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: RVSUM_1:13 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_rvsum_1 :::"+"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r2")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:14 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ))))) ; theorem :: RVSUM_1:15 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "F2")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F3"))))) ; theorem :: RVSUM_1:16 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k5_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; theorem :: RVSUM_1:17 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ))))) ; definitionlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"-"::: redefine func :::"-"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 5 (Set (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#k3_relat_1 :::"*"::: ) "F"); end; :: deftheorem defines :::"-"::: RVSUM_1:def 5 : (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set (Var "F"))))); definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); :: original: :::"-"::: redefine func :::"-"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:18 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ))))) ; theorem :: RVSUM_1:19 (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: RVSUM_1:20 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "r")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:21 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "r")) ")" ))))) ; theorem :: RVSUM_1:22 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k5_rvsum_1 :::"+"::: ) (Set "(" ($#k7_rvsum_1 :::"-"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: RVSUM_1:23 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set ($#k7_rvsum_1 :::"-"::: ) (Set (Var "R2")))))) ; theorem :: RVSUM_1:24 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "R2"))))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2")))) ; theorem :: RVSUM_1:25 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2"))))) ; theorem :: RVSUM_1:26 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )))) ; definitionlet "F1", "F2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"-"::: redefine func "F1" :::"-"::: "F2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 6 (Set (Set ($#k34_binop_2 :::"diffreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" "F1" "," "F2" ")" ); end; :: deftheorem defines :::"-"::: RVSUM_1:def 6 : (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k34_binop_2 :::"diffreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); :: original: :::"-"::: redefine func "R1" :::"-"::: "R2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:27 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R2")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "R2")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" )))))) ; theorem :: RVSUM_1:28 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set (Set (Var "F")) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ")" )) ; theorem :: RVSUM_1:29 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k8_rvsum_1 :::"-"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r2")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:30 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r1")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r1")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r2")) ")" ))))) ; theorem :: RVSUM_1:31 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:32 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k9_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R"))))) ; theorem :: RVSUM_1:33 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k7_rvsum_1 :::"-"::: ) (Set (Var "R")))))) ; theorem :: RVSUM_1:34 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2"))))) ; theorem :: RVSUM_1:35 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F1"))))) ; theorem :: RVSUM_1:36 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2"))))) ; theorem :: RVSUM_1:37 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: RVSUM_1:38 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2"))))) ; theorem :: RVSUM_1:39 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "F2")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F3")) ")" )))) ; theorem :: RVSUM_1:40 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "F2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F3"))))) ; theorem :: RVSUM_1:41 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "F2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F3"))))) ; theorem :: RVSUM_1:42 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R")) ")" ) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R")))))) ; theorem :: RVSUM_1:43 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R")) ")" ) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R")))))) ; notationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym "r" :::"*"::: "F" for "r" :::"(#)"::: "F"; end; theorem :: RVSUM_1:44 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k24_valued_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" )))))) ; definitionlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*"::: redefine func "r" :::"*"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 7 (Set (Set "(" "r" ($#k3_rvsum_1 :::"multreal"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "F"); end; :: deftheorem defines :::"*"::: RVSUM_1:def 7 : (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k3_rvsum_1 :::"multreal"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "F")))))); definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*"::: redefine func "r" :::"*"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:45 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" )))))) ; theorem :: RVSUM_1:46 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: RVSUM_1:47 (Bool "for" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r1")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:48 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "r1")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ))))) ; theorem :: RVSUM_1:49 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RVSUM_1:50 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RVSUM_1:51 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: RVSUM_1:52 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Num 1) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "F")))) ; theorem :: RVSUM_1:53 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: RVSUM_1:54 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F"))))) ; notationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); synonym :::"sqr"::: "F" for "F" :::"^2"::: ; end; definitionlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"sqr"::: redefine func :::"sqr"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 8 (Set (Set ($#k2_rvsum_1 :::"sqrreal"::: ) ) ($#k3_relat_1 :::"*"::: ) "F"); end; :: deftheorem defines :::"sqr"::: RVSUM_1:def 8 : (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rvsum_1 :::"sqrreal"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set (Var "F"))))); definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); :: original: :::"sqr"::: redefine func :::"sqr"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:55 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:56 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ))))) ; theorem :: RVSUM_1:57 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F"))))) ; theorem :: RVSUM_1:58 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F")) ")" ))))) ; notationlet "F1", "F2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); synonym :::"mlt"::: "(" "F1" "," "F2" ")" for "F1" :::"(#)"::: "F2"; end; definitionlet "F1", "F2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"mlt"::: redefine func :::"mlt"::: "(" "F1" "," "F2" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 9 (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" "F1" "," "F2" ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F2")) "," (Set (Var "F1")) ")" )))) ; end; :: deftheorem defines :::"mlt"::: RVSUM_1:def 9 : (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); theorem :: RVSUM_1:59 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ))))) ; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); :: original: :::"mlt"::: redefine func :::"mlt"::: "(" "R1" "," "R2" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: RVSUM_1:60 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ))))) ; theorem :: RVSUM_1:61 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: RVSUM_1:62 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r2")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; theorem :: RVSUM_1:63 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "R"))))))) ; theorem :: RVSUM_1:64 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r1")) ")" ) "," (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ))))) ; theorem :: RVSUM_1:65 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F1")) ")" ) "," (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:66 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) "," (Set (Var "R")) ")" ))))) ; theorem :: RVSUM_1:67 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F")) "," (Set (Var "F")) ")" ))) ; theorem :: RVSUM_1:68 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "F1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Num 2) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) ")" ) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:69 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "F1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F1")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Num 2) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) ")" ) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:70 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F2")) ")" ) ")" ))) ; notationlet "F" be ($#m1_hidden :::"Relation":::); synonym :::"complex-yielding"::: "F" for :::"complex-valued"::: ; end; registration cluster -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "F" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"Sum"::: "F" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) means :: RVSUM_1:def 10 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) "F") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f")))) ")" )); end; :: deftheorem defines :::"Sum"::: RVSUM_1:def 10 : (Bool "for" (Set (Var "F")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f")))) ")" )) ")" ))); registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k16_rvsum_1 :::"Sum"::: ) "F") -> ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: RVSUM_1:71 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))) ; definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"Sum"::: redefine func :::"Sum"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: RVSUM_1:def 11 (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) "F"); end; :: deftheorem defines :::"Sum"::: RVSUM_1:def 11 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))); definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"Sum"::: redefine func :::"Sum"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 12 (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) "F"); end; :: deftheorem defines :::"Sum"::: RVSUM_1:def 12 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))); theorem :: RVSUM_1:72 (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: RVSUM_1:73 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: RVSUM_1:74 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")))))) ; theorem :: RVSUM_1:75 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F1")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:76 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RVSUM_1:77 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2"))))) ; theorem :: RVSUM_1:78 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r3"))))) ; theorem :: RVSUM_1:79 (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: RVSUM_1:80 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r")))))) ; theorem :: RVSUM_1:81 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: RVSUM_1:82 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "R1")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "R2")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R2")))))) ; theorem :: RVSUM_1:83 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "R1")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "R2")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))) ")" ) & (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "R1")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "R2")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))) ")" ))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R2")))))) ; theorem :: RVSUM_1:84 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F"))))) ; theorem :: RVSUM_1:85 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F"))))) ; theorem :: RVSUM_1:86 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "F")) ")" )))) ; theorem :: RVSUM_1:87 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RVSUM_1:88 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" )))) ; theorem :: RVSUM_1:89 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: RVSUM_1:90 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: RVSUM_1:91 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k13_rvsum_1 :::"sqr"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: RVSUM_1:92 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k15_rvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k13_rvsum_1 :::"sqr"::: ) (Set (Var "R1")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k13_rvsum_1 :::"sqr"::: ) (Set (Var "R2")) ")" ) ")" ))))) ; definitionlet "F" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"Product"::: "F" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) means :: RVSUM_1:def 13 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) "F") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f")))) ")" )); end; :: deftheorem defines :::"Product"::: RVSUM_1:def 13 : (Bool "for" (Set (Var "F")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f")))) ")" )) ")" ))); registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k19_rvsum_1 :::"Product"::: ) "F") -> ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: RVSUM_1:93 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))) ; definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"Product"::: redefine func :::"Product"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: RVSUM_1:def 14 (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) "F"); end; :: deftheorem defines :::"Product"::: RVSUM_1:def 14 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k20_rvsum_1 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))); definitionlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"Product"::: redefine func :::"Product"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: RVSUM_1:def 15 (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) "F"); end; :: deftheorem defines :::"Product"::: RVSUM_1:def 15 : (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))); theorem :: RVSUM_1:94 (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ; registrationlet "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "r" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "r1", "r2" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "r1" "," "r2" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "r1", "r2", "r3" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k11_finseq_1 :::"<*"::: ) "r1" "," "r2" "," "r3" ($#k11_finseq_1 :::"*>"::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; theorem :: RVSUM_1:95 (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; registrationlet "f", "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k7_finseq_1 :::"^"::: ) "g") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; theorem :: RVSUM_1:96 (Bool "for" (Set (Var "F")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "F")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "r")))))) ; theorem :: RVSUM_1:97 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "F1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F2")) ")" )))) ; theorem :: RVSUM_1:98 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RVSUM_1:99 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "r2"))))) ; theorem :: RVSUM_1:100 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "r3"))))) ; theorem :: RVSUM_1:101 (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: RVSUM_1:102 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: RVSUM_1:103 (Bool "for" (Set (Var "F")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "iff" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: RVSUM_1:104 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Set (Var "j")) ")" ) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) ")" ))))) ; theorem :: RVSUM_1:105 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k24_binop_2 :::"*"::: ) (Set (Var "j")) ")" ) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k2_finseq_2 :::"|->"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) ")" ) ")" ))))) ; theorem :: RVSUM_1:106 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "r1")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r1")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r2")) ")" ) ")" ))))) ; theorem :: RVSUM_1:107 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" ($#k15_rvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "R1")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: RVSUM_1:108 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "r")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "R")) ")" )))))) ; theorem :: RVSUM_1:109 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k21_rvsum_1 :::"Product"::: ) (Set "(" ($#k13_rvsum_1 :::"sqr"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rvsum_1 :::"Product"::: ) (Set (Var "R")) ")" ) ($#k5_square_1 :::"^2"::: ) )))) ; begin theorem :: RVSUM_1:110 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k20_rvsum_1 :::"Product"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F"))))) ; theorem :: RVSUM_1:111 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z")) ")" ) ")" ))))) ; theorem :: RVSUM_1:112 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k24_binop_2 :::"*"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))))) ; theorem :: RVSUM_1:113 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "z1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k20_rvsum_1 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "z2")) ")" ) ")" ))))) ; begin theorem :: RVSUM_1:114 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))))) ; theorem :: RVSUM_1:115 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "x1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))))) ; theorem :: RVSUM_1:116 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "x1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))))) ; theorem :: RVSUM_1:117 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))))) ; theorem :: RVSUM_1:118 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))))) "holds" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; begin definitionlet "x1", "x2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"|(":::"x1" "," "x2":::")|"::: -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: RVSUM_1:def 16 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" "x1" "," "x2" ")" ")" )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x2")) "," (Set (Var "x1")) ")" ")" ))))) ; end; :: deftheorem defines :::"|("::: RVSUM_1:def 16 : (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k22_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k22_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" )))); definitionlet "x1", "x2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); :: original: :::"|("::: redefine func :::"|(":::"x1" "," "x2":::")|"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); commutativity (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k22_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k22_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k22_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x1")) ($#k22_rvsum_1 :::")|"::: ) ))) ; end; theorem :: RVSUM_1:119 (Bool "for" (Set (Var "x")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: RVSUM_1:120 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:121 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "a")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:122 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:123 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k23_rvsum_1 :::")|"::: ) ))) ; theorem :: RVSUM_1:124 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x3"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:125 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x3"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "x1")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ))))) ; theorem :: RVSUM_1:126 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:127 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:128 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:129 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:130 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:131 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))))) ; theorem :: RVSUM_1:132 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_rvsum_1 :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:133 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_rvsum_1 :::"-"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k7_rvsum_1 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k23_rvsum_1 :::")|"::: ) )))) ; theorem :: RVSUM_1:134 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:135 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k5_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "p2")) ")" ) ")" ) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "p3")) ($#k23_rvsum_1 :::")|"::: ) ) ")" )))))) ; theorem :: RVSUM_1:136 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:137 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "q1")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "q2")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p1")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q1")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p2")) "," (Set (Var "q2")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:138 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k5_rvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:139 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" (Set (Var "p")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "p")) ($#k9_rvsum_1 :::"-"::: ) (Set (Var "q")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; theorem :: RVSUM_1:140 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ))))) ; definitionlet "p", "q" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); pred "p" "," "q" :::"are_orthogonal"::: means :: RVSUM_1:def 17 (Bool (Set ($#k23_rvsum_1 :::"|("::: ) "p" "," "q" ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; end; :: deftheorem defines :::"are_orthogonal"::: RVSUM_1:def 17 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) ) "iff" (Bool (Set ($#k23_rvsum_1 :::"|("::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k23_rvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); theorem :: RVSUM_1:141 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k11_rvsum_1 :::"*"::: ) (Set (Var "p"))) "," (Set (Var "q")) ($#r1_rvsum_1 :::"are_orthogonal"::: ) )))) ; theorem :: RVSUM_1:142 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "," (Set (Var "r4")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "," (Set (Var "r4")) ($#k7_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r1")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r3")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "r4"))))) ; theorem :: RVSUM_1:143 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: RVSUM_1:144 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "f")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set (Var "g")) ")" )))) ; theorem :: RVSUM_1:145 (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ))) ;