:: MATRIXJ2  semantic presentation begin  

















definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "n" be   ($#m1_hidden :::"Nat":::); func  :::"Jordan_block":::  "(" "L" "," "n" ")"  ->   ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIXJ2:def 1 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  "n") & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  it)  ($#r1_hidden :::"="::: )  "n") & (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"::: )  it))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  "L")  ")"  &  "("  (Bool (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  "K"))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "K"))  ")"   ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"Jordan_block"::: MATRIXJ2:def 1 :  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (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 "b4"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "b4"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "L")))  ")"  &  "("  (Bool (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "b4"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "K"))))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j"))) & (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "b4"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")"   ")" )  ")" )  ")" )  ")" ))))); 
 definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"Jordan_block"::: redefine func  :::"Jordan_block":::  "(" "L" "," "n" ")"  ->   ($#m1_matrix_1 :::"Upper_Triangular_Matrix":::) "of" "n" "," "K"; end; 
theorem :: MATRIXJ2:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k13_matrix_3 :::"diagonal_of_Matrix"::: )  (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "L"))))))) ; 
 
theorem :: MATRIXJ2:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_group_1 :::"power"::: )  (Set (Var "K")) ")" )  ($#k1_laplace :::"."::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: MATRIXJ2:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" ) "is"   ($#v1_matrix_6 :::"invertible"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) "or" (Bool (Set (Var "L"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")" )  ")" )))) ; 
 
theorem :: MATRIXJ2:4 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k10_fvsum_1 :::"*"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#k4_fvsum_1 :::"+"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )))))) ; 
 
theorem :: MATRIXJ2:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k10_fvsum_1 :::"*"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: MATRIXJ2:6 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "K"))))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n")))) "implies" (Bool (Set (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "implies" (Bool (Set (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"   ")" ))))) ; 
 
theorem :: MATRIXJ2:7 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "K"))))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1))) "implies" (Bool (Set (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "implies" (Bool (Set (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k8_group_1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "F"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" )))  ")"   ")" ))))) ; 
 
theorem :: MATRIXJ2:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "L"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))) "holds"  (Bool  "ex" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st"  (Bool  "("  (Bool (Set (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" )  ($#k5_matrix_6 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (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  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_group_1 :::"power"::: )  (Set (Var "K")) ")" )  ($#k1_laplace :::"."::: )   "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "L"))  ($#k11_algstr_0 :::"""::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )))  ")"   ")" )  ")" )  ")" ))))) ; 
 
theorem :: MATRIXJ2:9 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" )  ($#k5_matrlin2 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k2_matrix13 :::"*"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set  "(" (Set (Var "L"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a")) ")" ) "," (Set (Var "n")) ")" ))))) ; 
 begin  definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "G" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "K")))  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ); attr "G" is  :::"Jordan-block-yielding":::  means :: MATRIXJ2:def 2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "G"))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" "K"(Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set "G"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" ))))); end; 





:: deftheorem    defines :::"Jordan-block-yielding"::: MATRIXJ2:def 2 :  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "G")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "K")))  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_matrixj2 :::"Jordan-block-yielding"::: )  ) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))(Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" )))))  ")" ))); 
 registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   bbbadV2_FUNCOP_1()   ($#v1_matrixj2 :::"Jordan-block-yielding"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ); 
end; registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); 
cluster   ($#v1_matrixj2 :::"Jordan-block-yielding"::: )    ->   ($#v2_matrixj1 :::"Square-Matrix-yielding"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ); 
end; definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); mode FinSequence_of_Jordan_block of "K" is   ($#v1_matrixj2 :::"Jordan-block-yielding"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ); end; definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); mode  :::"FinSequence_of_Jordan_block":::  "of" "L" "," "K" ->   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" "K" means :: MATRIXJ2:def 3 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set it  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" "L" "," (Set (Var "n")) ")" )))); end; 






:: deftheorem    defines :::"FinSequence_of_Jordan_block"::: MATRIXJ2:def 3 :  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K"))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "b3"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" ))))  ")" )))); 
 
theorem :: MATRIXJ2:10 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K"))))) ; 
 
theorem :: MATRIXJ2:11 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set  ($#k16_matrixj1 :::"<*"::: ) (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")"  ")" ) ($#k16_matrixj1 :::"*>"::: ) ) "is"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K")))))) ; 
 registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"non-empty"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   bbbadV2_FUNCOP_1()   ($#v1_matrixj1 :::"Matrix-yielding"::: )     ($#v2_matrixj1 :::"Square-Matrix-yielding"::: )     ($#v1_matrixj2 :::"Jordan-block-yielding"::: )    for    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" "L" "," "K"; 
end; registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"non-empty"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   bbbadV2_FUNCOP_1()   ($#v1_matrixj1 :::"Matrix-yielding"::: )     ($#v2_matrixj1 :::"Square-Matrix-yielding"::: )     ($#v1_matrixj2 :::"Jordan-block-yielding"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#k3_finseq_2 :::"*"::: )  ")" )  ($#k3_finseq_2 :::"*"::: )  ); 
end; 
theorem :: MATRIXJ2:12 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K")) "holds"  (Bool (Set (Set (Var "J"))  ($#k25_matrixj1 :::"(+)"::: )  (Set  "("  ($#k24_matrixj1 :::"mlt"::: )   "(" (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "J")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "a")) ")" ) "," (Set  "("  ($#k23_matrixj1 :::"1."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set (Var "J")) ")" ) ")"  ")" ) ")"  ")" )) "is"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Set (Var "L"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "a"))) "," (Set (Var "K")))))) ; 
 definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "J1", "J2" be   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" (Set (Const "K")); :: original: :::"^"::: redefine func "J1" :::"^"::: "J2" ->   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" "K"; end; definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "n" be   ($#m1_hidden :::"Nat":::); let "J" be   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" (Set (Const "K")); :: original: :::"|"::: redefine func "J" :::"|"::: "n" ->   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" "K"; :: original: :::"/^"::: redefine func "J" :::"/^"::: "n" ->   ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" "K"; end; definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "J1", "J2" be    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Const "L")) "," (Set (Const "K")); :: original: :::"^"::: redefine func "J1" :::"^"::: "J2" ->    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" "L" "," "K"; end; definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "L" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "n" be   ($#m1_hidden :::"Nat":::); let "J" be    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Const "L")) "," (Set (Const "K")); :: original: :::"|"::: redefine func "J" :::"|"::: "n" ->    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" "L" "," "K"; :: original: :::"/^"::: redefine func "J" :::"/^"::: "n" ->    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" "L" "," "K"; end; begin  definitionlet "K" be    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "f" is  :::"nilpotent":::  means :: MATRIXJ2:def 4 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "holds"  (Bool (Set (Set  "(" "f"  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V")))); end; 






:: deftheorem    defines :::"nilpotent"::: MATRIXJ2:def 4 :  (Bool  "for" (Set (Var "K")) "being"    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_matrixj2 :::"nilpotent"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))))  ")" )))); 
 
theorem :: MATRIXJ2:13 (Bool  "for" (Set (Var "K")) "being"    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_matrixj2 :::"nilpotent"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" (Set (Var "V")) "," (Set (Var "V")) ")" )))  ")" )))) ; 
 registrationlet "K" be    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))   ($#v2_matrixj2 :::"nilpotent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "V" be   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_mod_2 :::"homogeneous"::: )     ($#v2_matrixj2 :::"nilpotent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: MATRIXJ2:14 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )) "is"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"linear-transformation":::) "of" (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )))))) ; 
 definitionlet "K" be    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); func  :::"degree_of_nilpotent"::: "f" ->   ($#m1_hidden :::"Nat":::) means :: MATRIXJ2:def 5 (Bool  "("  (Bool (Set "f"  ($#k1_vectsp11 :::"|^"::: )  it)  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" "V" "," "V" ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set "f"  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" "V" "," "V" ")" ))) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" ); end; 







:: deftheorem    defines :::"degree_of_nilpotent"::: MATRIXJ2:def 5 :  (Bool  "for" (Set (Var "K")) "being"    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrixj2 :::"degree_of_nilpotent"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "b4")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" (Set (Var "V")) "," (Set (Var "V")) ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" (Set (Var "V")) "," (Set (Var "V")) ")" ))) "holds"  (Bool (Set (Var "b4"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))  ")" )  ")" )  ")" ))))); 
 notationlet "K" be    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "K")); let "f" be   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); synonym  :::"deg"::: "f" for  :::"degree_of_nilpotent"::: "f"; end; 
theorem :: MATRIXJ2:15 (Bool  "for" (Set (Var "K")) "being"    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) "iff" (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) ))  ")" )))) ; 
 
theorem :: MATRIXJ2:16 (Bool  "for" (Set (Var "K")) "being"    ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V")) (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))))))) ; 
 
theorem :: MATRIXJ2:17 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k7_matrlin2 :::"|"::: )  (Set (Var "W"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "W")) "," (Set (Var "W")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_matrlin2 :::"|"::: )  (Set (Var "W"))) "is"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "W")) "," (Set (Var "W"))))))) ; 
 
theorem :: MATRIXJ2:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "fI")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "fI"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k9_matrixj2 :::"deg"::: )  (Set (Var "fI")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "f")))))))))) ; 
 




































theorem :: MATRIXJ2:19 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "B2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "bw1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "W1"))  (Bool  "for" (Set (Var "bw2")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "W2"))  (Bool  "for" (Set (Var "Bu1")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "Bu2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U2"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B2"))) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M1")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "bw1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bu1"))) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M2")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "bw2"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bu2"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "bw1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "bw2")))) & (Bool (Set (Var "B2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Bu1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "Bu2")))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_matrixj1 :::"block_diagonal"::: )   "(" (Set  ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" )) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bu1")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "M2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bu2"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "bw1"))))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M1")) "," (Set (Var "bw1")) "," (Set (Var "Bu1")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "bw1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "bw2"))))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "bw1")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M2")) "," (Set (Var "bw2")) "," (Set (Var "Bu2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "bw2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"   ")" ))))))))))))))) ; 
 
theorem :: MATRIXJ2:20 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "B2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B2"))) "," (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "F")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b1")))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrixj1 :::"min"::: )   "(" (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "("  ($#k5_matrlin :::"lmlt"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k2_matrixj1 :::"."::: )  (Set (Var "m")) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set  "(" (Set (Var "F"))  ($#k6_matrixj1 :::"|"::: )  (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ")"  ")" ) "," (Set  "(" (Set  "(" (Set (Var "B2"))  ($#k17_finseq_1 :::"|"::: )  (Set  "("  ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k11_matrixj1 :::"Width"::: )  (Set  "(" (Set (Var "F"))  ($#k6_matrixj1 :::"|"::: )  (Set (Var "m")) ")" ) ")" ) ")" ) ")" )  ($#k2_rfinseq :::"/^"::: )  (Set  "("  ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k11_matrixj1 :::"Width"::: )  (Set  "(" (Set (Var "F"))  ($#k6_matrixj1 :::"|"::: )  (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ")"  ")" ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set  "(" (Set (Var "B2"))  ($#k17_finseq_1 :::"|"::: )  (Set  "("  ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k11_matrixj1 :::"Width"::: )  (Set  "(" (Set (Var "F"))  ($#k6_matrixj1 :::"|"::: )  (Set (Var "m")) ")" ) ")" ) ")" ) ")" )  ($#k2_rfinseq :::"/^"::: )  (Set  "("  ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k11_matrixj1 :::"Width"::: )  (Set  "(" (Set (Var "F"))  ($#k6_matrixj1 :::"|"::: )  (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "(" (Set (Var "F"))  ($#k2_matrixj1 :::"."::: )  (Set (Var "m")) ")" )))  ")" )))))))) ; 
 
theorem :: MATRIXJ2:21 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "B1")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "B1"))))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "("  ($#k5_matrlin :::"lmlt"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1")) ")" ) ")"  ")" ) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1")) ")" ) ")"  ")" ) "," (Set (Var "B1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B1"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1")) ")" ) ")" ))))))) ; 
 
theorem :: MATRIXJ2:22 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "B1")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "B1")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1"))))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "("  ($#k5_matrlin :::"lmlt"::: )   "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "("  ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "B1")) ")" ) ")"  ")" ) "," (Set (Var "i")) ")"  ")" ) "," (Set (Var "B1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "B1"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))))))) ; 
 
theorem :: MATRIXJ2:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "B2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B2"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set (Var "n")) ")" ))) "holds"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b1"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")"   ")" ))))))))) ; 
 
theorem :: MATRIXJ2:24 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "B2")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B2"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b1")))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrixj1 :::"min"::: )   "(" (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set (Var "J")) ")" ) "," (Set (Var "i")) ")" ))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set  "(" (Set (Var "J"))  ($#k7_matrixj2 :::"|"::: )  (Set (Var "m")) ")" ) ")" )))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set  "(" (Set (Var "J"))  ($#k7_matrixj2 :::"|"::: )  (Set (Var "m")) ")" ) ")" )))) "implies" (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "B2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")"   ")" ))))))))) ; 
 
theorem :: MATRIXJ2:25 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))) "holds"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "J"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "J"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")"  ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "m")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k6_grcat_1 :::"ZeroMap"::: )   "(" (Set (Var "V1")) "," (Set (Var "V1")) ")" )))))))) ; 
 
theorem :: MATRIXJ2:26 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" ) "is"   ($#v2_matrixj2 :::"nilpotent"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) "or" (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")" )  ")" ))))))) ; 
 
theorem :: MATRIXJ2:27 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))) "," (Set (Var "K"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1"))) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "F"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" ))) "holds"  (Bool  "("  (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "J")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "J"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "F"))))  ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "J"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "J"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k9_matrixj2 :::"deg"::: )  (Set (Var "F"))))  ")" )  ")" ))))))) ; 
 
theorem :: MATRIXJ2:28 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2"))))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b1")))) "or" (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "b2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))) "or" (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b1")))) & (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "b1"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "(" (Set (Var "b2"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b2"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" )) "holds"  (Bool  "ex" (Set (Var "J")) "being"   ($#v2_relat_1 :::"non-empty"::: )     ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K")) "st" (Bool (Set   ($#k1_matrlin2 :::"AutMt"::: )   "(" (Set (Var "F")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))))))))) ; 
 
theorem :: MATRIXJ2:29 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#v2_matrixj2 :::"nilpotent"::: )    ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) (Bool  "ex" (Set (Var "J")) "being"   ($#v2_relat_1 :::"non-empty"::: )     ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))) "," (Set (Var "K"))(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1")) "st" (Bool (Set   ($#k1_matrlin2 :::"AutMt"::: )   "(" (Set (Var "F")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))))))) ; 
 
theorem :: MATRIXJ2:30 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "V1")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "F1")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set  "(" (Set (Var "F"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "F"))  ($#k8_matrlin2 :::"|"::: )  (Set (Var "V1")))  ($#r1_funct_2 :::"="::: )  (Set (Var "F1")))) "holds"  (Bool  "ex" (Set (Var "J")) "being"   ($#v2_relat_1 :::"non-empty"::: )     ($#m1_matrixj2 :::"FinSequence_of_Jordan_block"::: )   "of" (Set (Var "L")) "," (Set (Var "K"))(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1")) "st" (Bool (Set   ($#k1_matrlin2 :::"AutMt"::: )   "(" (Set (Var "F1")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" ))))))))))) ; 
 begin  
theorem :: MATRIXJ2:31 (Bool  "for" (Set (Var "K")) "being"   ($#v2_polynom5 :::"algebraic-closed"::: )    ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "V")) (Bool  "ex" (Set (Var "J")) "being"   ($#v2_relat_1 :::"non-empty"::: )    ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" (Set (Var "K"))(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set   ($#k1_matrlin2 :::"AutMt"::: )   "(" (Set (Var "F")) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")" )) & (Bool  "("   "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "F"))) "iff" (Bool  "ex" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "J")))) & (Bool (Set (Set (Var "J"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixj2 :::"Jordan_block"::: )   "(" (Set (Var "L")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "J"))  ($#k14_matrixj1 :::"."::: )  (Set (Var "i")) ")" ) ")" ) ")" ))  ")" ))  ")" )  ")" )  ")" )))))) ; 
 
theorem :: MATRIXJ2:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#v2_polynom5 :::"algebraic-closed"::: )    ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool  "ex" (Set (Var "J")) "being"   ($#v2_relat_1 :::"non-empty"::: )    ($#m2_finseq_1 :::"FinSequence_of_Jordan_block":::) "of" (Set (Var "K"))(Bool  "ex" (Set (Var "P")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st"  (Bool  "("  (Bool (Set   ($#k2_wsierp_1 :::"Sum"::: )  (Set  "("  ($#k10_matrixj1 :::"Len"::: )  (Set (Var "J")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "P")) "is"   ($#v1_matrix_6 :::"invertible"::: )  ) & (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "K")) ")" ) ")"  ")" ) ")" )  ($#k4_matrix_3 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k5_matrix_6 :::"~"::: )  ")" )))  ")" )))))) ;