:: MATRIXC1 semantic presentation begin definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func "M" :::"*'"::: -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" ) ")" ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" ) ")" )) ; end; :: deftheorem defines :::"*'"::: MATRIXC1:def 1 : (Bool "for" (Set (Var "M")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k15_complex1 :::"*'"::: ) )) ")" ) ")" ) ")" )); theorem :: MATRIXC1:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#v1_matrix_1 :::"tabular"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) ")" ) ")" ))) ; theorem :: MATRIXC1:2 canceled; theorem :: MATRIXC1:3 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "a")) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "a")) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) ")" ))) ; theorem :: MATRIXC1:4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" )))))) ; theorem :: MATRIXC1:5 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M")) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k7_matrix_5 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ))))) ; theorem :: MATRIXC1:6 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "M1")) ($#k3_matrix_5 :::"+"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "M1")) ($#k3_matrix_5 :::"+"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")))) ")" )) ; theorem :: MATRIXC1:7 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k3_matrix_5 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "M2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIXC1:8 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k3_matrix_5 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k1_matrixc1 :::"*'"::: ) ")" ) ($#k3_matrix_5 :::"+"::: ) (Set "(" (Set (Var "M2")) ($#k1_matrixc1 :::"*'"::: ) ")" )))) ; theorem :: MATRIXC1:9 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k4_matrix_5 :::"-"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k4_matrix_5 :::"-"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) ")" )) ; theorem :: MATRIXC1:10 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" ($#k4_matrix_5 :::"-"::: ) (Set (Var "M")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIXC1:11 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_5 :::"-"::: ) (Set (Var "M"))))) ; theorem :: MATRIXC1:12 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_matrix_5 :::"-"::: ) (Set (Var "M")) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_5 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" )))) ; theorem :: MATRIXC1:13 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_5 :::"-"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_5 :::"-"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")))) ")" )) ; theorem :: MATRIXC1:14 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_5 :::"-"::: ) (Set (Var "M2")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "M2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIXC1:15 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_5 :::"-"::: ) (Set (Var "M2")) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k1_matrixc1 :::"*'"::: ) ")" ) ($#k5_matrix_5 :::"-"::: ) (Set "(" (Set (Var "M2")) ($#k1_matrixc1 :::"*'"::: ) ")" )))) ; definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func "M" :::"@""::: -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 2 (Set (Set "(" "M" ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k1_matrixc1 :::"*'"::: ) ); end; :: deftheorem defines :::"@""::: MATRIXC1:def 2 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "M")) ($#k2_matrixc1 :::"@""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k1_matrixc1 :::"*'"::: ) ))); definitionlet "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); assume (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"FinSeq2Matrix"::: "x" -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "x")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "x" ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" "x" ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"FinSeq2Matrix"::: MATRIXC1:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrixc1 :::"FinSeq2Matrix"::: ) (Set (Var "x")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) ")" ) ")" ))); definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Matrix2FinSeq"::: "M" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 4 (Set ($#k9_matrix_1 :::"Col"::: ) "(" "M" "," (Num 1) ")" ); end; :: deftheorem defines :::"Matrix2FinSeq"::: MATRIXC1:def 4 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k4_matrixc1 :::"Matrix2FinSeq"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Num 1) ")" ))); definitionlet "F1", "F2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"mlt"::: "(" "F1" "," "F2" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 5 (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" "F1" "," "F2" ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "F2")) "," (Set (Var "F1")) ")" ))) ; end; :: deftheorem defines :::"mlt"::: MATRIXC1:def 5 : (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ))); definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func "M" :::"*"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "M" ")" )))) "holds" (Bool (Set it ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "M" "," (Set (Var "i")) ")" ")" ) "," "F" ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"*"::: MATRIXC1:def 6 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k6_matrixc1 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "F")) ")" ")" ))) ")" ) ")" ) ")" ))); theorem :: MATRIXC1:16 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (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 "a")) ($#k12_seq_4 :::"*"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "R1")) ")" ) "," (Set (Var "R2")) ")" ))))) ; definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "M" :::"*"::: "a" -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 7 (Set "a" ($#k7_matrix_5 :::"*"::: ) "M"); end; :: deftheorem defines :::"*"::: MATRIXC1:def 7 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "M")) ($#k7_matrixc1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k7_matrix_5 :::"*"::: ) (Set (Var "M")))))); theorem :: MATRIXC1:17 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k7_matrixc1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k7_matrix_5 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ))))) ; theorem :: MATRIXC1:18 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#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: :::"mlt"::: redefine func :::"mlt"::: "(" "R1" "," "R2" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); end; theorem :: MATRIXC1:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" ) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "R2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ))))) ; theorem :: MATRIXC1:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k15_complex1 :::"*'"::: ) ")" ) ")" ")" ) ($#k15_complex1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) "," (Set (Var "b")) ")" ))) ; theorem :: MATRIXC1:21 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k9_matrix_5 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k9_matrix_5 :::"."::: ) (Set (Var "n"))))))) ; theorem :: MATRIXC1:22 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "F")) ($#k1_complsp2 :::"*'"::: ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set "(" (Set (Var "F")) ($#k1_complsp2 :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F")) ")" ) ($#k15_complex1 :::"*'"::: ) ))) ; theorem :: MATRIXC1:23 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k1_complsp2 :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k15_complex1 :::"*'"::: ) ))) ; theorem :: MATRIXC1:24 (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 "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "x")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ))) ; theorem :: MATRIXC1:25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: MATRIXC1:26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: MATRIXC1:27 (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 "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_complsp2 :::"*'"::: ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ))) ; theorem :: MATRIXC1:28 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k12_seq_4 :::"*"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; definitionlet "x" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"FR2FC"::: "x" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 8 "x"; end; :: deftheorem defines :::"FR2FC"::: MATRIXC1:def 8 : (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_matrixc1 :::"FR2FC"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))); theorem :: MATRIXC1:29 (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "F")))))) ; theorem :: MATRIXC1:30 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "y")))))) ; theorem :: MATRIXC1:31 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2"))))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F1")) ($#k10_seq_4 :::"-"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F1")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F2")) ")" )))) ; theorem :: MATRIXC1:32 (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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" (Set (Var "x")) ($#k10_seq_4 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ($#k10_seq_4 :::"-"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; theorem :: MATRIXC1:33 (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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k10_seq_4 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k10_seq_4 :::"-"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" )))) ; theorem :: MATRIXC1:34 (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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k9_seq_4 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" )))) ; theorem :: MATRIXC1:35 (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 ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" (Set (Var "x")) ($#k9_seq_4 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; theorem :: MATRIXC1:36 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2"))))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F1")) ($#k9_seq_4 :::"+"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F1")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F2")) ")" )))) ; theorem :: MATRIXC1:37 (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 ($#k29_binop_2 :::"multcomplex"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x1")) "," (Set (Var "y1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )))) ; theorem :: MATRIXC1:38 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k9_matrixc1 :::"FR2FC"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" ($#k9_matrixc1 :::"FR2FC"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k9_matrixc1 :::"FR2FC"::: ) (Set (Var "y")) ")" ) ")" ))) ; theorem :: MATRIXC1:39 (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 (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ")" )))) ; theorem :: MATRIXC1:40 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")) ")" )))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M1")) ($#k3_matrix_5 :::"+"::: ) (Set (Var "M2")) ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "j")) ")" ")" ) ($#k9_seq_4 :::"+"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M2")) "," (Set (Var "j")) ")" ")" ))))) ; theorem :: MATRIXC1:41 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_complsp2 :::"*'"::: ) )))) ; theorem :: MATRIXC1:42 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" ")" ) ($#k1_complsp2 :::"*'"::: ) ))))) ; theorem :: MATRIXC1:43 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k6_matrixc1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_complsp2 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) ($#k6_matrixc1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_complsp2 :::"*'"::: ) ")" ))))) ; theorem :: MATRIXC1:44 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F3"))))) "holds" (Bool (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F2")) "," (Set (Var "F3")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixc1 :::"mlt"::: ) "(" (Set "(" ($#k5_matrixc1 :::"mlt"::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ")" ) "," (Set (Var "F3")) ")" ))) ; theorem :: MATRIXC1:45 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_seq_4 :::"-"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" )))) ; theorem :: MATRIXC1:46 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "F1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F1")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F2")) ")" )))) ; definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"LineSum"::: "M" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 9 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "M" ")" )))) "holds" (Bool (Set it ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "M" "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"LineSum"::: MATRIXC1:def 9 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixc1 :::"LineSum"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ) ")" ))); definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"ColSum"::: "M" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 10 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool (Set it ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" "M" "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"ColSum"::: MATRIXC1:def 10 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixc1 :::"ColSum"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" ))); theorem :: MATRIXC1:47 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k9_matrix_5 :::"."::: ) (Num 1)))) ; theorem :: MATRIXC1:48 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_rvsum_1 :::"Sum"::: ) (Set (Var "g")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ))))) ; theorem :: MATRIXC1:49 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k10_matrixc1 :::"LineSum"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k11_matrixc1 :::"ColSum"::: ) (Set (Var "M")) ")" )))) ; definitionlet "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"SumAll"::: "M" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIXC1:def 11 (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k10_matrixc1 :::"LineSum"::: ) "M" ")" )); end; :: deftheorem defines :::"SumAll"::: MATRIXC1:def 11 : (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k12_matrixc1 :::"SumAll"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k17_rvsum_1 :::"Sum"::: ) (Set "(" ($#k10_matrixc1 :::"LineSum"::: ) (Set (Var "M")) ")" )))); theorem :: MATRIXC1:50 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k11_matrixc1 :::"ColSum"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixc1 :::"LineSum"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" )))) ; theorem :: MATRIXC1:51 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k12_matrixc1 :::"SumAll"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrixc1 :::"SumAll"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" )))) ; definitionlet "x", "y" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); assume that (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "M")))) and (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")))) ; func :::"QuadraticForm"::: "(" "x" "," "M" "," "y" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIXC1:def 12 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "x")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "y")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "x" ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set "(" "y" ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k15_complex1 :::"*'"::: ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"QuadraticForm"::: MATRIXC1:def 12 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "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 "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "x")) "," (Set (Var "M")) "," (Set (Var "y")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k9_matrix_5 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k9_matrix_5 :::"."::: ) (Set (Var "j")) ")" ) ($#k15_complex1 :::"*'"::: ) ")" ))) ")" ) ")" ) ")" )))); theorem :: MATRIXC1:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "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 "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "x")) "," (Set (Var "M")) "," (Set (Var "y")) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "M")) ($#k2_matrixc1 :::"@""::: ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k1_matrixc1 :::"*'"::: ) )))) ; theorem :: MATRIXC1:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "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 "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "x")) "," (Set (Var "M")) "," (Set (Var "y")) ")" ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set "(" (Set (Var "x")) ($#k1_complsp2 :::"*'"::: ) ")" ) "," (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_complsp2 :::"*'"::: ) ")" ) ")" )))) ; theorem :: MATRIXC1:54 (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")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "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 :: MATRIXC1:55 (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")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#k15_complex1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "x")) ($#k1_complsp2 :::"*'"::: ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_complsp2 :::"*'"::: ) ")" ) ($#k8_complsp2 :::")|"::: ) ))) ; theorem :: MATRIXC1:56 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k1_matrixc1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k1_matrixc1 :::"*'"::: ) ")" ) ($#k4_matrix_1 :::"@"::: ) ))) ; theorem :: MATRIXC1:57 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "M")) ($#k2_matrixc1 :::"@""::: ) ")" ) ($#k6_matrixc1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrixc1 :::"SumAll"::: ) (Set "(" ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: MATRIXC1:58 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "M")) ($#k6_matrixc1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrixc1 :::"SumAll"::: ) (Set "(" ($#k13_matrixc1 :::"QuadraticForm"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: MATRIXC1:59 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set (Var "M")) ($#k6_matrixc1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set "(" (Set (Var "M")) ($#k2_matrixc1 :::"@""::: ) ")" ) ($#k6_matrixc1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) )))) ; theorem :: MATRIXC1:60 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "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 "M")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_complsp2 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "M")) ($#k6_matrixc1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complsp2 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_complsp2 :::"|("::: ) (Set "(" (Set "(" (Set (Var "M")) ($#k2_matrixc1 :::"@""::: ) ")" ) ($#k6_matrixc1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k8_complsp2 :::")|"::: ) )))) ;