:: MATRIX_5  semantic presentation begin  
theorem :: MATRIX_5:1 (Bool (Num 1)  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ))) ; 
 
theorem :: MATRIX_5:2 (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k1_complfld :::"F_Complex"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 definitionlet "A" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func  :::"COMPLEX2Field"::: "A" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) equals :: MATRIX_5:def 1 "A"; end; 





:: deftheorem    defines :::"COMPLEX2Field"::: MATRIX_5:def 1 :  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set   ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))); 
 definitionlet "A" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ); func  :::"Field2COMPLEX"::: "A" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 2 "A"; end; 





:: deftheorem    defines :::"Field2COMPLEX"::: MATRIX_5:def 2 :  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"  (Bool (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))); 
 
theorem :: MATRIX_5:3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set   ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: MATRIX_5:4 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: MATRIX_5:5 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" )))) ; 
 
theorem :: MATRIX_5:6 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set  "("  ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "A")) ")" )))) ; 
 definitionlet "A", "B" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func "A" :::"+"::: "B" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 3 (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "A" ")" )  ($#k3_matrix_3 :::"+"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "B" ")" ) ")" )); end; 






:: deftheorem    defines :::"+"::: MATRIX_5:def 3 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" )  ($#k3_matrix_3 :::"+"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "B")) ")" ) ")" )))); 
 definitionlet "A" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func  :::"-"::: "A" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 4 (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "("  ($#k2_matrix_3 :::"-"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "A" ")" ) ")" )); end; 





:: deftheorem    defines :::"-"::: MATRIX_5:def 4 :  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set   ($#k4_matrix_5 :::"-"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "("  ($#k2_matrix_3 :::"-"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" ) ")" )))); 
 definitionlet "A", "B" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func "A" :::"-"::: "B" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 5 (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "A" ")" )  ($#k1_matrix_4 :::"-"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "B" ")" ) ")" )); func "A" :::"*"::: "B" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 6 (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "A" ")" )  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "B" ")" ) ")" )); end; 












:: deftheorem    defines :::"-"::: MATRIX_5:def 5 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set (Var "A"))  ($#k5_matrix_5 :::"-"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" )  ($#k1_matrix_4 :::"-"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "B")) ")" ) ")" )))); 
 
:: deftheorem    defines :::"*"::: MATRIX_5:def 6 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_matrix_5 :::"*"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" )  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "B")) ")" ) ")" )))); 
 definitionlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "A" be   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ); func "x" :::"*"::: "A" ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: MATRIX_5:def 7 (Bool  "for" (Set (Var "ea")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set (Var "ea"))  ($#r1_hidden :::"="::: )  "x")) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set (Var "ea"))  ($#k6_matrix_3 :::"*"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  "A" ")" ) ")" )))); end; 






:: deftheorem    defines :::"*"::: MATRIX_5:def 7 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k7_matrix_5 :::"*"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "ea")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) )  "st" (Bool (Bool (Set (Var "ea"))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "(" (Set (Var "ea"))  ($#k6_matrix_3 :::"*"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" ) ")" ))))  ")" ))); 
 
theorem :: MATRIX_5:7 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set (Var "A")) ")" )))  ")" )) ; 
 
theorem :: MATRIX_5:8 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "A")) ")" ))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set (Var "A")) ")" )))  ")" )) ; 
 
theorem :: MATRIX_5:9 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "("  ($#k1_group_1 :::"1_"::: )  (Set (Var "K")) ")" )  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))))) ; 
 
theorem :: MATRIX_5:10 (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Num 1)  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) ; 
 
theorem :: MATRIX_5:11 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_matrix_3 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M"))))))) ; 
 
theorem :: MATRIX_5:12 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M")) ")" )  ($#k3_matrix_3 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M")) ")" )))))) ; 
 
theorem :: MATRIX_5:13 (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set (Var "M"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M"))))) ; 
 
theorem :: MATRIX_5:14 (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "M"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M")) ")" )  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M"))))) ; 
 definitionlet "n", "m" be   ($#m1_hidden :::"Nat":::); func  :::"0_Cx":::  "(" "n" "," "m" ")"  ->   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) equals :: MATRIX_5:def 8 (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "("  ($#k1_matrix_3 :::"0."::: )   "(" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "," "n" "," "m" ")"  ")" )); end; 






:: deftheorem    defines :::"0_Cx"::: MATRIX_5:def 8 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_5 :::"Field2COMPLEX"::: )  (Set  "("  ($#k1_matrix_3 :::"0."::: )   "(" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) "," (Set (Var "m")) ")"  ")" )))); 
 
theorem :: MATRIX_5:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_matrix_5 :::"COMPLEX2Field"::: )  (Set  "("  ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_3 :::"0."::: )   "(" (Set  ($#k1_complfld :::"F_Complex"::: ) ) "," (Set (Var "n")) "," (Set (Var "m")) ")" ))) ; 
 
theorem :: MATRIX_5:16 (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 (Var "M1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M1"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M2"))))) "holds"  (Bool (Set (Var "M2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")" ))) ; 
 
theorem :: MATRIX_5:17 (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 (Set (Var "M1"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M2")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")" ))) "holds"  (Bool (Set (Var "M2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrix_5 :::"-"::: )  (Set (Var "M1"))))) ; 
 
theorem :: MATRIX_5:18 (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 (Set (Var "M2"))  ($#k5_matrix_5 :::"-"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set (Var "M2")))) "holds"  (Bool (Set (Var "M1"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")" ))) ; 
 
theorem :: MATRIX_5:19 (Bool  "for" (Set (Var "M")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"  (Bool (Set (Set (Var "M"))  ($#k3_matrix_5 :::"+"::: )  (Set  "("  ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) ; 
 
theorem :: MATRIX_5:20 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "M1")) "," (Set (Var "M2")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "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 (Var "b"))  ($#k6_matrix_3 :::"*"::: )  (Set  "(" (Set (Var "M1"))  ($#k3_matrix_3 :::"+"::: )  (Set (Var "M2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M1")) ")" )  ($#k3_matrix_3 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M2")) ")" )))))) ; 
 
theorem :: MATRIX_5:21 (Bool  "for" (Set (Var "M1")) "," (Set (Var "M2")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "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 (Var "a"))  ($#k7_matrix_5 :::"*"::: )  (Set  "(" (Set (Var "M1"))  ($#k3_matrix_5 :::"+"::: )  (Set (Var "M2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M1")) ")" )  ($#k3_matrix_5 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M2")) ")" ))))) ; 
 
theorem :: MATRIX_5:22 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M1")) "," (Set (Var "M2")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")"  ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "M2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M2")) ")" ) ")" )))) ; 
 
theorem :: MATRIX_5:23 (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   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")"  ")" )  ($#k6_matrix_5 :::"*"::: )  (Set (Var "M2")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M2")) ")" ) ")" ))) ; 
 
theorem :: MATRIX_5:24 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M1")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" )  ($#k6_matrix_3 :::"*"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")" )))) ; 
 
theorem :: MATRIX_5:25 (Bool  "for" (Set (Var "M1")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k2_numbers :::"COMPLEX"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k7_matrix_5 :::"*"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_5 :::"0_Cx"::: )   "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M1")) ")" ) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")) ")" ) ")" ))) ; 
 definitionlet "s" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); let "k" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"."::: redefine func "s" :::"."::: "k" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); end; 
theorem :: MATRIX_5:26 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"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 "M2")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2")))) & (Bool (Set (Set (Var "s"))  ($#k9_matrix_5 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "M1"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "(" (Set (Var "M2"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Set (Var "j")) ")"  ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M2"))))) "holds"  (Bool (Set (Set (Var "s"))  ($#k9_matrix_5 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k9_matrix_5 :::"."::: )  (Set (Var "k")) ")" )  ($#k3_binop_2 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "M1"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k5_binop_2 :::"*"::: )  (Set  "(" (Set (Var "M2"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "j")) ")"  ")" ) ")" )))  ")" )  ")" )))) ;