:: RVSUM_2  semantic presentation begin  definitionlet "F" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Relation":::); :: original: :::"rng"::: redefine func  :::"rng"::: "F" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set (Const "D")); let "F1" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); 
cluster (Set "F1"  ($#k3_relat_1 :::"(#)"::: )  "F") ->   ($#v1_finseq_1 :::"FinSequence-like"::: )   ; 
end; 



























definitionfunc  :::"sqrcomplex":::  ->   ($#m1_subset_1 :::"UnOp":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: RVSUM_2:def 1 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_square_1 :::"^2"::: )  ))); end; 




:: deftheorem    defines :::"sqrcomplex"::: RVSUM_2:def 1 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"UnOp":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rvsum_2 :::"sqrcomplex"::: )  )) "iff" (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_square_1 :::"^2"::: )  )))  ")" )); 
 
theorem :: RVSUM_2:1 (Bool (Set   ($#k2_rvsum_2 :::"sqrcomplex"::: )  )  ($#r7_binop_1 :::"is_distributive_wrt"::: )  (Set   ($#k29_binop_2 :::"multcomplex"::: )  )) ; 
 
theorem :: RVSUM_2:2 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "c"))  ($#k7_seq_4 :::"multcomplex"::: )  )  ($#r7_binop_1 :::"is_distributive_wrt"::: )  (Set   ($#k27_binop_2 :::"addcomplex"::: )  ))) ; 
 begin  definitionlet "F1", "F2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); :: original: :::"+"::: redefine func "F1" :::"+"::: "F2" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: RVSUM_2:def 2 (Set (Set  ($#k27_binop_2 :::"addcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" "F1" "," "F2" ")" ); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k27_binop_2 :::"addcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k27_binop_2 :::"addcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F2")) "," (Set (Var "F1")) ")" ))))
 ; end; 






:: deftheorem    defines :::"+"::: RVSUM_2:def 2 :  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set (Var "F1"))  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "F2")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k27_binop_2 :::"addcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); 
 definitionlet "i" be   ($#m1_hidden :::"Nat":::); let "R1", "R2" be (Set (Const "i"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"+"::: redefine func "R1" :::"+"::: "R2" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "i"  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )); end; 
theorem :: RVSUM_2:3 (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" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "R1"))  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set  "(" (Set (Var "R2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")) ")" )))))) ; 
 
theorem :: RVSUM_2:4 (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )))) ; 
 
theorem :: RVSUM_2:5 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c1")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k3_rvsum_2 :::"+"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c2")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "c1"))  ($#k3_binop_2 :::"+"::: )  (Set (Var "c2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RVSUM_2:6 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c1")) ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "(" (Set (Var "c1"))  ($#k3_binop_2 :::"+"::: )  (Set (Var "c2")) ")" ))))) ; 
 definitionlet "F" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); :: original: :::"-"::: redefine func  :::"-"::: "F" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: RVSUM_2:def 3 (Set (Set  ($#k25_binop_2 :::"compcomplex"::: ) )  ($#k3_relat_1 :::"*"::: )  "F"); end; 





:: deftheorem    defines :::"-"::: RVSUM_2:def 3 :  (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k25_binop_2 :::"compcomplex"::: ) )  ($#k3_relat_1 :::"*"::: )  (Set (Var "F"))))); 
 definitionlet "i" be   ($#m1_hidden :::"Nat":::); let "R" be (Set (Const "i"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"-"::: redefine func  :::"-"::: "R" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "i"  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )); end; 
theorem :: RVSUM_2:7 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "("  ($#k1_binop_2 :::"-"::: )  (Set (Var "c")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RVSUM_2:8 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "("  ($#k1_binop_2 :::"-"::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: RVSUM_2:9 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R")) "," (Set (Var "R2")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Set (Var "R1"))  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R2"))  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R"))))) "holds"  (Bool (Set (Var "R1"))  ($#r1_hidden :::"="::: )  (Set (Var "R2"))))) ; 
 
theorem :: RVSUM_2:10 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "F1"))  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_rvsum_2 :::"-"::: )  (Set (Var "F1")) ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set  "("  ($#k5_rvsum_2 :::"-"::: )  (Set (Var "F2")) ")" )))) ; 
 definitionlet "F1", "F2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); :: original: :::"-"::: redefine func "F1" :::"-"::: "F2" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: RVSUM_2:def 4 (Set (Set  ($#k28_binop_2 :::"diffcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" "F1" "," "F2" ")" ); end; 






:: deftheorem    defines :::"-"::: RVSUM_2:def 4 :  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set (Var "F1"))  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "F2")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k28_binop_2 :::"diffcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); 
 definitionlet "i" be   ($#m1_hidden :::"Nat":::); let "R1", "R2" be (Set (Const "i"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"-"::: redefine func "R1" :::"-"::: "R2" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "i"  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )); end; 
theorem :: RVSUM_2: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" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "R1"))  ($#k8_rvsum_2 :::"-"::: )  (Set (Var "R2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")) ")" )  ($#k4_binop_2 :::"-"::: )  (Set  "(" (Set (Var "R2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")) ")" )))))) ; 
 
theorem :: RVSUM_2:12 (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" )  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ))) & (Bool (Set (Set (Var "F"))  ($#k7_rvsum_2 :::"-"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )))  ")" )) ; 
 
theorem :: RVSUM_2:13 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c1")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_rvsum_2 :::"-"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c2")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "c1"))  ($#k4_binop_2 :::"-"::: )  (Set (Var "c2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RVSUM_2:14 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c1")) ")" )  ($#k7_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "(" (Set (Var "c1"))  ($#k4_binop_2 :::"-"::: )  (Set (Var "c2")) ")" ))))) ; 
 
theorem :: RVSUM_2:15 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "R"))  ($#k8_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k5_complex1 :::"0c"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "R"))))) ; 
 
theorem :: RVSUM_2:16 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "F1"))  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F2"))  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "F1"))))) ; 
 
theorem :: RVSUM_2:17 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k5_rvsum_2 :::"-"::: )  (Set  "(" (Set (Var "F1"))  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_rvsum_2 :::"-"::: )  (Set (Var "F1")) ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "F2"))))) ; 
 
theorem :: RVSUM_2:18 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Set (Var "R1"))  ($#k8_rvsum_2 :::"-"::: )  (Set (Var "R2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k5_complex1 :::"0c"::: ) )))) "holds"  (Bool (Set (Var "R1"))  ($#r1_hidden :::"="::: )  (Set (Var "R2"))))) ; 
 
theorem :: RVSUM_2:19 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Var "R1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R1"))  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R")) ")" )  ($#k8_rvsum_2 :::"-"::: )  (Set (Var "R")))))) ; 
 
theorem :: RVSUM_2:20 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Var "R1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R1"))  ($#k8_rvsum_2 :::"-"::: )  (Set (Var "R")) ")" )  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R")))))) ; 
 notationlet "F" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); let "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; synonym "c" :::"*"::: "F" for "c" :::"(#)"::: "F"; end; definitionlet "F" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); let "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"*"::: redefine func "c" :::"*"::: "F" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: RVSUM_2:def 5 (Set (Set  "(" "c"  ($#k7_seq_4 :::"multcomplex"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  "F"); end; 






:: deftheorem    defines :::"*"::: RVSUM_2:def 5 :  (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "c"))  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c"))  ($#k7_seq_4 :::"multcomplex"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "F")))))); 
 definitionlet "i" be   ($#m1_hidden :::"Nat":::); let "R" be (Set (Const "i"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); let "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"*"::: redefine func "c" :::"*"::: "R" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "i"  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )); end; 
theorem :: RVSUM_2:21 (Bool  "for" (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "c"))  ($#k9_rvsum_2 :::"*"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c1")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "c"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c1")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RVSUM_2:22 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "c1"))  ($#k9_rvsum_2 :::"*"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "(" (Set (Var "c1"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c2")) ")" ))))) ; 
 
theorem :: RVSUM_2:23 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "c1"))  ($#k3_binop_2 :::"+"::: )  (Set (Var "c2")) ")" )  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c1"))  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "F")) ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set  "(" (Set (Var "c2"))  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "F")) ")" ))))) ; 
 
theorem :: RVSUM_2:24 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set  ($#k5_complex1 :::"0c"::: ) )  ($#k10_rvsum_2 :::"*"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k5_complex1 :::"0c"::: ) ))))) ; 
 notationlet "F1", "F2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); synonym  :::"mlt":::  "(" "F1" "," "F2" ")"  for "F1" :::"(#)"::: "F2"; end; definitionlet "F1", "F2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); :: original: :::"mlt"::: redefine func  :::"mlt":::  "(" "F1" "," "F2" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: RVSUM_2:def 6 (Set (Set  ($#k29_binop_2 :::"multcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" "F1" "," "F2" ")" ); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k29_binop_2 :::"multcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k29_binop_2 :::"multcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F2")) "," (Set (Var "F1")) ")" ))))
 ; end; 






:: deftheorem    defines :::"mlt"::: RVSUM_2:def 6 :  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k29_binop_2 :::"multcomplex"::: ) )  ($#k3_funcop_1 :::".:"::: )   "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); 
 definitionlet "i" be   ($#m1_hidden :::"Nat":::); let "R1", "R2" be (Set (Const "i"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"mlt"::: redefine func  :::"mlt":::  "(" "R1" "," "R2" ")"  ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "i"  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )); end; 
theorem :: RVSUM_2:25 (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" ) "," (Set (Var "F")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )))) ; 
 
theorem :: RVSUM_2:26 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c1")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c2")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "c1"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c2")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RVSUM_2:27 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ) "," (Set (Var "R")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k10_rvsum_2 :::"*"::: )  (Set (Var "R"))))))) ; 
 
theorem :: RVSUM_2:28 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c1")) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c2")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "(" (Set (Var "c1"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c2")) ")" ))))) ; 
 begin  
theorem :: RVSUM_2:29 (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) ; 
 
theorem :: RVSUM_2:30 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) ; 
 
theorem :: RVSUM_2:31 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "F"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "F")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set (Var "c")))))) ; 
 
theorem :: RVSUM_2:32 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v1_valued_0 :::"complex-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")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "F2")) ")" )))) ; 
 
theorem :: RVSUM_2:33 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "(" (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_binop_2 :::"+"::: )  (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "F")) ")" ))))) ; 
 
theorem :: RVSUM_2:34 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k10_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c1"))  ($#k3_binop_2 :::"+"::: )  (Set (Var "c2"))))) ; 
 
theorem :: RVSUM_2:35 (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) ($#k11_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "c1"))  ($#k3_binop_2 :::"+"::: )  (Set (Var "c2")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set (Var "c3"))))) ; 
 
theorem :: RVSUM_2:36 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c")))))) ; 
 
theorem :: RVSUM_2:37 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k5_complex1 :::"0c"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) ; 
 
theorem :: RVSUM_2:38 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "c"))  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "F")) ")" ))))) ; 
 
theorem :: RVSUM_2:39 (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k5_rvsum_2 :::"-"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_binop_2 :::"-"::: )  (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "F")) ")" )))) ; 
 
theorem :: RVSUM_2:40 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "R1"))  ($#k4_rvsum_2 :::"+"::: )  (Set (Var "R2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_rvsum_1 :::"Sum"::: )  (Set (Var "R1")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set  "("  ($#k17_rvsum_1 :::"Sum"::: )  (Set (Var "R2")) ")" ))))) ; 
 
theorem :: RVSUM_2:41 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k17_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "R1"))  ($#k8_rvsum_2 :::"-"::: )  (Set (Var "R2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_rvsum_1 :::"Sum"::: )  (Set (Var "R1")) ")" )  ($#k4_binop_2 :::"-"::: )  (Set  "("  ($#k17_rvsum_1 :::"Sum"::: )  (Set (Var "R2")) ")" ))))) ; 
 begin  
theorem :: RVSUM_2:42 (Bool (Set   ($#k20_rvsum_1 :::"Product"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: RVSUM_2:43 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k9_finseq_1 :::"*>"::: ) )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set (Var "F")) ")" ))))) ; 
 
theorem :: RVSUM_2:44 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k2_numbers :::"COMPLEX"::: ) )) "holds"  (Bool (Set   ($#k20_rvsum_1 :::"Product"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: RVSUM_2:45 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#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 "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ) ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "j"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ) ")" ))))) ; 
 
theorem :: RVSUM_2:46 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#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 "c")) ")" ))  ($#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 "c")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: RVSUM_2:47 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k20_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k5_finseq_2 :::"|->"::: )  (Set  "(" (Set (Var "c1"))  ($#k5_binop_2 :::"*"::: )  (Set (Var "c2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c1")) ")" ) ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c2")) ")" ) ")" ))))) ; 
 
theorem :: RVSUM_2:48 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k20_rvsum_1 :::"Product"::: )  (Set  "("  ($#k12_rvsum_2 :::"mlt"::: )   "(" (Set (Var "R1")) "," (Set (Var "R2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_rvsum_1 :::"Product"::: )  (Set (Var "R1")) ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k20_rvsum_1 :::"Product"::: )  (Set (Var "R2")) ")" ))))) ; 
 
theorem :: RVSUM_2:49 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "R")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k20_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "c"))  ($#k10_rvsum_2 :::"*"::: )  (Set (Var "R")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "i"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "c")) ")" ) ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "("  ($#k20_rvsum_1 :::"Product"::: )  (Set (Var "R")) ")" )))))) ; 
 begin  
theorem :: RVSUM_2:50 (Bool  "for" (Set (Var "x")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k5_rvsum_2 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x"))))) ; 
 
theorem :: RVSUM_2:51 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#v1_valued_0 :::"complex-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"))  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "x2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1"))))) ; 
 
theorem :: RVSUM_2:52 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#v1_valued_0 :::"complex-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"))  ($#k7_rvsum_2 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1"))))) ; 
 
theorem :: RVSUM_2:53 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "a"))  ($#k9_rvsum_2 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))))) ; 
 
theorem :: RVSUM_2:54 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_valued_0 :::"complex-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   ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set  "(" (Set (Var "x"))  ($#k3_rvsum_2 :::"+"::: )  (Set (Var "y")) ")" ) "," (Set (Var "z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set (Var "x")) "," (Set (Var "z")) ")"  ")" )  ($#k3_rvsum_2 :::"+"::: )  (Set  "("  ($#k11_rvsum_2 :::"mlt"::: )   "(" (Set (Var "y")) "," (Set (Var "z")) ")"  ")" )))) ;