:: COMPLSP2 semantic presentation begin definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func "z" :::"*'"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: COMPLSP2:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "z")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "z"))) "holds" (Bool (Set it ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "z" ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"*'"::: COMPLSP2:def 1 : (Bool "for" (Set (Var "z")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_complsp2 :::"*'"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" ) ")" ) ")" )); theorem :: COMPLSP2:1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ))))) ; theorem :: COMPLSP2:2 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (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; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (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; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*"::: redefine func "r" :::"*"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); end; theorem :: COMPLSP2:3 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))))) ; theorem :: COMPLSP2:4 (Bool "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" )))) ; theorem :: COMPLSP2:5 (Bool "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))))) ; theorem :: COMPLSP2:6 (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")) ($#k1_valued_1 :::"+"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))))) ; theorem :: COMPLSP2:7 (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")) ($#k45_valued_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))))) ; theorem :: COMPLSP2:8 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k14_seq_4 :::"COMPLEX"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) ; theorem :: COMPLSP2:9 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 ($#k2_numbers :::"COMPLEX"::: ) )) "holds" (Bool (Set (Set (Var "R1")) ($#k2_complsp2 :::"-"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k9_seq_4 :::"+"::: ) (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: COMPLSP2:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLSP2:11 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) "holds" (Bool (Set (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k4_complsp2 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k11_seq_4 :::"-"::: ) (Set (Var "R")))))) ; theorem :: COMPLSP2:12 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_seq_4 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_seq_4 :::"-"::: ) (Set (Var "x"))))) ; theorem :: COMPLSP2:13 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (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 :: COMPLSP2:14 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k5_complsp2 :::"-"::: ) (Set (Var "R")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "c"))))))) ; theorem :: COMPLSP2:15 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x")))))) ; theorem :: COMPLSP2:16 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" )))))) ; theorem :: COMPLSP2:17 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complsp2 :::"*'"::: ) ")" ))))) ; theorem :: COMPLSP2:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 ($#k2_numbers :::"COMPLEX"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k3_complsp2 :::"+"::: ) (Set (Var "R2")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "R2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ))))) ; theorem :: COMPLSP2:19 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k1_complsp2 :::"*'"::: ) ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k1_complsp2 :::"*'"::: ) ")" )))) ; theorem :: COMPLSP2:20 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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 ($#k2_numbers :::"COMPLEX"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k2_complsp2 :::"-"::: ) (Set (Var "R2")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "R2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ))))) ; theorem :: COMPLSP2:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k1_complsp2 :::"*'"::: ) ")" ) ($#k10_seq_4 :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k1_complsp2 :::"*'"::: ) ")" )))) ; theorem :: COMPLSP2:22 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_complsp2 :::"*'"::: ) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: COMPLSP2:23 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k11_seq_4 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k1_complsp2 :::"*'"::: ) ")" )))) ; theorem :: COMPLSP2:24 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k15_complex1 :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLSP2:25 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ))))) ; theorem :: COMPLSP2:26 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ))))) ; definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Re"::: "z" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: COMPLSP2:def 2 (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k12_seq_4 :::"*"::: ) (Set "(" "z" ($#k9_seq_4 :::"+"::: ) (Set "(" "z" ($#k1_complsp2 :::"*'"::: ) ")" ) ")" )); end; :: deftheorem defines :::"Re"::: COMPLSP2:def 2 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k6_complsp2 :::"Re"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" )))); theorem :: COMPLSP2:27 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k15_complex1 :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) )))) ; definitionlet "z" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Im"::: "z" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: COMPLSP2:def 3 (Set (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k12_seq_4 :::"*"::: ) (Set "(" "z" ($#k10_seq_4 :::"-"::: ) (Set "(" "z" ($#k1_complsp2 :::"*'"::: ) ")" ) ")" )); end; :: deftheorem defines :::"Im"::: COMPLSP2:def 3 : (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k7_complsp2 :::"Im"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k10_seq_4 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" )))); definitionlet "x", "y" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"|(":::"x" "," "y":::")|"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: COMPLSP2:def 4 (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) "x" ")" ) "," (Set "(" ($#k6_complsp2 :::"Re"::: ) "y" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) "x" ")" ) "," (Set "(" ($#k7_complsp2 :::"Im"::: ) "y" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) "x" ")" ) "," (Set "(" ($#k6_complsp2 :::"Re"::: ) "y" ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) "x" ")" ) "," (Set "(" ($#k7_complsp2 :::"Im"::: ) "y" ")" ) ($#k23_rvsum_1 :::")|"::: ) )); end; :: deftheorem defines :::"|("::: COMPLSP2:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k23_rvsum_1 :::"|("::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "y")) ")" ) ($#k23_rvsum_1 :::")|"::: ) )))); theorem :: COMPLSP2:28 (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 (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_valued_1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set (Var "z"))))) ; theorem :: COMPLSP2:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_valued_1 :::"+"::: ) (Set (Var "x"))))) ; theorem :: COMPLSP2:30 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ))))) ; theorem :: COMPLSP2:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLSP2:32 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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 (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "y")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "x")))) ")" )) ; theorem :: COMPLSP2:33 (Bool "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: COMPLSP2:34 (Bool "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" )))) ; theorem :: COMPLSP2:35 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLSP2:36 (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 (Set "(" (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k1_valued_1 :::"+"::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLSP2:37 (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 (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k45_valued_1 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_valued_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set (Var "z"))))) ; theorem :: COMPLSP2:38 canceled; theorem :: COMPLSP2:39 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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"))))) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set (Var "y"))))) ; theorem :: COMPLSP2:40 (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 (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k45_valued_1 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k45_valued_1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set (Var "z"))))) ; theorem :: COMPLSP2:41 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set "(" ($#k17_seq_4 :::"0c"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_seq_4 :::"0c"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ))))) ; theorem :: COMPLSP2:42 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k11_seq_4 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x")) ")" ))))) ; theorem :: COMPLSP2:43 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) ($#k10_seq_4 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ))))) ; theorem :: COMPLSP2:44 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )))) ; theorem :: COMPLSP2:45 (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x1"))))) "holds" (Bool (Set (Set (Var "C")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "x1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "x2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "y2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "C")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )))))) ; theorem :: COMPLSP2:46 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )))) ; theorem :: COMPLSP2:47 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set (Var "x1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "y2")))))) ; theorem :: COMPLSP2:48 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) ")" )) ; theorem :: COMPLSP2:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set ($#k6_complsp2 :::"Re"::: ) (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "y")) ")" ))) & (Bool (Set ($#k7_complsp2 :::"Im"::: ) (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "y")) ")" ))) ")" )) ; theorem :: COMPLSP2:50 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set ($#k28_binop_2 :::"diffcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k34_binop_2 :::"diffreal"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )))) ; theorem :: COMPLSP2:51 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set (Var "x1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "y2")))))) ; theorem :: COMPLSP2:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set ($#k6_complsp2 :::"Re"::: ) (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "y")) ")" ))) & (Bool (Set ($#k7_complsp2 :::"Im"::: ) (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "y")) ")" ))) ")" )) ; theorem :: COMPLSP2:53 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")))))) ; theorem :: COMPLSP2:54 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) ($#k12_seq_4 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_seq_4 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ))))) ; theorem :: COMPLSP2:55 (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "y1"))))) "holds" (Bool (Set (Set (Var "h")) ($#k9_matrix_5 :::"."::: ) (Set "(" (Set (Var "y1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "y2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k4_finseqop :::"*"::: ) (Set (Var "y2")))))))) ; theorem :: COMPLSP2:56 (Bool "for" (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set ($#k25_binop_2 :::"compcomplex"::: ) ) ($#k4_finseqop :::"*"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#k4_finseqop :::"*"::: ) (Set (Var "y2")))))) ; theorem :: COMPLSP2:57 (Bool "for" (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k11_seq_4 :::"-"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set (Var "y2")))))) ; theorem :: COMPLSP2:58 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_complsp2 :::"Re"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k7_complsp2 :::"Im"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")))) ")" )) ; theorem :: COMPLSP2:59 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:60 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ")" )))) ; theorem :: COMPLSP2:61 (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k7_seq_4 :::"multcomplex"::: ) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a2")) ($#k3_rvsum_1 :::"multreal"::: ) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "y2")))))))) ; theorem :: COMPLSP2:62 (Bool "for" (Set (Var "a1")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "y1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set (Set (Var "a1")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "y2")))))))) ; theorem :: COMPLSP2:63 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k12_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" ))))) ; theorem :: COMPLSP2:64 (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k12_seq_4 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ($#k10_seq_4 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" ))))) ; theorem :: COMPLSP2:65 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_complsp2 :::"Re"::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "a")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "a")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set ($#k7_complsp2 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "a")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "x")) ")" ) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "a")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "x")) ")" ) ")" ))) ")" ))) ; begin theorem :: COMPLSP2:66 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:67 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set (Var "x2")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:68 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:69 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k8_complsp2 :::")|"::: ) ))) ; theorem :: COMPLSP2:70 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set (Var "x3")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x3")) ($#k8_complsp2 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "x3")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:71 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#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 ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:72 (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#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 ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:73 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:74 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y2")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:75 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k8_complsp2 :::")|"::: ) ) ($#k15_complex1 :::"*'"::: ) ))) ; theorem :: COMPLSP2:76 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k8_complsp2 :::")|"::: ) ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k8_complsp2 :::")|"::: ) ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "y")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: COMPLSP2:78 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ))))) ; theorem :: COMPLSP2:79 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ))))) ; theorem :: COMPLSP2:80 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 ($#k8_complsp2 :::"|("::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) "," (Set (Var "z")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k8_complsp2 :::")|"::: ) ) ")" ))))) ; theorem :: COMPLSP2:81 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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 ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k12_seq_4 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k8_complsp2 :::")|"::: ) ) ")" ))))) ;