:: VECTSP11  semantic presentation begin  

















theorem :: VECTSP11:1 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "nt")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ))  (Bool  "for" (Set (Var "mt")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "m"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ))  "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "nt")) ")" ) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "mt")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k1_matrix13 :::"Segm"::: )   "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_3 :::"+"::: )  (Set (Var "B")) ")" ) "," (Set (Var "nt")) "," (Set (Var "mt")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_matrix13 :::"Segm"::: )   "(" (Set (Var "A")) "," (Set (Var "nt")) "," (Set (Var "mt")) ")"  ")" )  ($#k5_matrlin2 :::"+"::: )  (Set  "("  ($#k1_matrix13 :::"Segm"::: )   "(" (Set (Var "B")) "," (Set (Var "nt")) "," (Set (Var "mt")) ")"  ")" )))))))) ; 
 
theorem :: VECTSP11:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "P")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_setfam_1 :::"without_zero"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k6_matrix13 :::"Segm"::: )   "(" (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "P")) "," (Set (Var "P")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "P")) ")" ) ")" ))))) ; 
 
theorem :: VECTSP11:3 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_setfam_1 :::"without_zero"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k6_matrix13 :::"Segm"::: )   "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_3 :::"+"::: )  (Set (Var "B")) ")" ) "," (Set (Var "P")) "," (Set (Var "Q")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_matrix13 :::"Segm"::: )   "(" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "Q")) ")"  ")" )  ($#k5_matrlin2 :::"+"::: )  (Set  "("  ($#k6_matrix13 :::"Segm"::: )   "(" (Set (Var "B")) "," (Set (Var "P")) "," (Set (Var "Q")) ")"  ")" )))))) ; 
 
theorem :: VECTSP11:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k2_laplace :::"Delete"::: )   "(" (Set  "(" (Set (Var "A"))  ($#k5_matrlin2 :::"+"::: )  (Set (Var "B")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_laplace :::"Delete"::: )   "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k5_matrlin2 :::"+"::: )  (Set  "("  ($#k2_laplace :::"Delete"::: )   "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )))))) ; 
 
theorem :: VECTSP11:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K"))  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k2_laplace :::"Delete"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k2_matrix13 :::"*"::: )  (Set (Var "A")) ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_matrix13 :::"*"::: )  (Set  "("  ($#k2_laplace :::"Delete"::: )   "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))))))) ; 
 
theorem :: VECTSP11:6 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k2_laplace :::"Delete"::: )   "(" (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )))) ; 
 
theorem :: VECTSP11:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "K")) "st"  (Bool  "("  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "P")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k2_polynom4 :::"eval"::: )   "(" (Set (Var "P")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrlin2 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k2_matrix13 :::"*"::: )  (Set (Var "B")) ")" ) ")" )))  ")" )  ")" ))))) ; 
 
theorem :: VECTSP11:8 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "K")) "st"  (Bool  "("  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k2_polynom4 :::"eval"::: )   "(" (Set (Var "P")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrlin2 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k2_matrix13 :::"*"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )))  ")" )  ")" ))))) ; 
 registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v1_matrlin :::"finite-dimensional"::: )    for    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" "K"; 
end; begin  definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "R")); let "IT" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "IT" is  :::"with_eigenvalues":::  means :: VECTSP11:def 1 (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V"(Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "R" "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V")) & (Bool (Set "IT"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v"))))  ")" ))); end; 






:: deftheorem    defines :::"with_eigenvalues"::: VECTSP11:def 1 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "R"))  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) "iff" (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))(Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set (Set (Var "IT"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v"))))  ")" )))  ")" )))); 
 



















registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); let "V" be  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (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"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v13_vectsp_1 :::"additive"::: )     ($#v1_mod_2 :::"homogeneous"::: )     ($#v1_vectsp11 :::"with_eigenvalues"::: )    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; definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "R")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); assume 
(Bool (Set (Const "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  )
 ; mode  :::"eigenvalue":::  "of" "f" ->   ($#m1_subset_1 :::"Element":::) "of" "R" means :: VECTSP11:def 2 (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" "V" "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V")) & (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set it  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v"))))  ")" )); end; 








:: deftheorem    defines :::"eigenvalue"::: VECTSP11:def 2 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "R"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  )) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "b4")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f"))) "iff" (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b4"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v"))))  ")" ))  ")" ))))); 
 definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l6_algstr_0 :::"doubleLoopStr"::: )  ; let "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Const "R")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "V")); let "L" be   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); assume 
(Bool  "("  (Bool (Set (Const "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Const "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Const "f")))  ")" )
 ; mode  :::"eigenvector":::  "of" "f" "," "L" ->   ($#m1_subset_1 :::"Vector":::) "of" "V" means :: VECTSP11:def 3 (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  it)  ($#r1_hidden :::"="::: )  (Set "L"  ($#k4_vectsp_1 :::"*"::: )  it)); end; 









:: deftheorem    defines :::"eigenvector"::: VECTSP11:def 3 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "R"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b5")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f")) "," (Set (Var "L"))) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b5")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "b5"))))  ")" )))))); 
 
theorem :: VECTSP11:9 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#v1_vectsp11 :::"with_eigenvalues"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k4_matrlin :::"*"::: )  (Set (Var "f"))) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "L"))) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Set (Var "a"))  ($#k4_matrlin :::"*"::: )  (Set (Var "f")))) &  "("  (Bool (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f")) "," (Set (Var "L")))) "implies" (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Set (Var "a"))  ($#k4_matrlin :::"*"::: )  (Set (Var "f"))) "," (Set (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "L"))))  ")"  &  "("  (Bool (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Set (Var "a"))  ($#k4_matrlin :::"*"::: )  (Set (Var "f"))) "," (Set (Set (Var "a"))  ($#k8_group_1 :::"*"::: )  (Set (Var "L"))))) "implies" (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f")) "," (Set (Var "L")))  ")"   ")" ))))))) ; 
 
theorem :: VECTSP11:10 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_vectsp11 :::"with_eigenvalues"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "V"))  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "L1")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f1"))) & (Bool (Set (Var "L2")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f2"))) & (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "v")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f1")) "," (Set (Var "L1"))) & (Bool (Set (Var "v")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f2")) "," (Set (Var "L2"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k3_matrlin :::"+"::: )  (Set (Var "f2"))) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Set (Var "L1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "L2"))) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Set (Var "f1"))  ($#k3_matrlin :::"+"::: )  (Set (Var "f2")))) & (Bool  "("   "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f1")) "," (Set (Var "L1"))) & (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f2")) "," (Set (Var "L2")))) "holds"  (Bool (Set (Var "w")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Set (Var "f1"))  ($#k3_matrlin :::"+"::: )  (Set (Var "f2"))) "," (Set (Set (Var "L1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "L2"))))  ")" )  ")" ))))) ; 
 
theorem :: VECTSP11:11 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "V"))) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "K"))) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "V")))) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Var "v")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "V"))) "," (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "K"))))  ")" )  ")" ))) ; 
 
theorem :: VECTSP11:12 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "V"))) "holds"  (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set (Var "K"))))))) ; 
 
theorem :: VECTSP11:13 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  "st" (Bool (Bool (Bool  "not" (Set   ($#k1_ranknull :::"ker"::: )  (Set (Var "f"))) "is"   ($#v7_struct_0 :::"trivial"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))  ")" )))) ; 
 
theorem :: VECTSP11:14 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))  ")" ) "iff" (Bool (Bool  "not" (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )) "is"   ($#v7_struct_0 :::"trivial"::: )  ))  ")" ))))) ; 
 
theorem :: VECTSP11:15 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "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")) "," (Set (Var "b19")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))  ")" ) "iff" (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k3_matrlin2 :::"AutEqMt"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ) "," (Set (Var "b1")) "," (Set (Var "b19")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "K"))))  ")" )))))) ; 
 
theorem :: VECTSP11:16 (Bool  "for" (Set (Var "K")) "being"   ($#v2_polynom5 :::"algebraic-closed"::: )    ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "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 "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  )))) ; 
 
theorem :: VECTSP11:17 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))) "holds"  (Bool  "("  (Bool (Set (Var "v1")) "is"    ($#m2_vectsp11 :::"eigenvector"::: )   "of" (Set (Var "f")) "," (Set (Var "L"))) "iff" (Bool (Set (Var "v1"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )))  ")" )))))) ; 
 definitionlet "S" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "S")); let "n" be   ($#m1_hidden :::"Nat":::); func "F" :::"|^"::: "n" ->   ($#m1_subset_1 :::"Function":::) "of" "S" "," "S" means :: VECTSP11:def 4 (Bool  "for" (Set (Var "F9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_monoid_0 :::"GFuncs"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ")" )  "st" (Bool (Bool (Set (Var "F9"))  ($#r1_hidden :::"="::: )  "F")) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k3_group_4 :::"Product"::: )  (Set  "(" "n"  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "F9")) ")" )))); end; 







:: deftheorem    defines :::"|^"::: VECTSP11:def 4 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")))) "iff" (Bool  "for" (Set (Var "F9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_monoid_0 :::"GFuncs"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  "st" (Bool (Bool (Set (Var "F9"))  ($#r1_hidden :::"="::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_group_4 :::"Product"::: )  (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "F9")) ")" ))))  ")" ))))); 
 






theorem :: VECTSP11:18 (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "S")))))) ; 
 
theorem :: VECTSP11:19 (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Num 1))  ($#r2_funct_2 :::"="::: )  (Set (Var "F"))))) ; 
 
theorem :: VECTSP11:20 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "j")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )))))) ; 
 
theorem :: VECTSP11:21 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "m")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "s2"))) & (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "s2")))) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_vectsp11 :::"|^"::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "s2")))))))) ; 
 
theorem :: VECTSP11:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_group_1 :::"associative"::: )     ($#v4_vectsp_1 :::"well-unital"::: )     ($#v5_vectsp_1 :::"distributive"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    (Bool  "for" (Set (Var "V1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" (Set (Var "K"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "fW")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "W")) "," (Set (Var "W"))  "st" (Bool (Bool (Set (Var "fW"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k7_matrlin2 :::"|"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k7_matrlin2 :::"|"::: )  (Set (Var "W")))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "fW"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")))))))))) ; 
 registrationlet "K" be   ($#l6_algstr_0 :::"Field":::); let "V1" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V1")); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "f"  ($#k1_vectsp11 :::"|^"::: )  "n") ->   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_mod_2 :::"homogeneous"::: )   ; 
end; 
theorem :: VECTSP11:23 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j")) ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1"))))))))) ; 
 begin  definitionlet "K" be   ($#l6_algstr_0 :::"Field":::); let "V1" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V1")); func  :::"UnionKers"::: "f" ->   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V1" means :: VECTSP11:def 5 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Vector":::) "of" "V1" : (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set  "(" "f"  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V1")))  "}"  ); end; 







:: deftheorem    defines :::"UnionKers"::: VECTSP11:def 5 :  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V1")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1")) : (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (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 "V1")))))  "}"  )  ")" ))))); 
 
theorem :: VECTSP11:24 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1")) "holds"   (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1")))))  ")" ))))) ; 
 
theorem :: VECTSP11:25 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))))))) ; 
 
theorem :: VECTSP11:26 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set  "(" (Set (Var "i"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "j")) ")" ) ")" ))))))) ; 
 
theorem :: VECTSP11:27 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#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 "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ))))))) ; 
 
theorem :: VECTSP11:28 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )) "is"   ($#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")) ")" ) ")" )))))) ; 
 
theorem :: VECTSP11:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )) "is"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ))))))) ; 
 
theorem :: VECTSP11:30 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")) ")" )) "is"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: VECTSP11:31 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ) ")" )) "is"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ) ")" ) "," (Set  "("  ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ) ")" )))))) ; 
 
theorem :: VECTSP11:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )) "is"   ($#m1_subset_1 :::"linear-transformation":::) "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")) ")" ) ")" )))))) ; 
 
theorem :: VECTSP11:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )) "is"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ) "," (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ))))))) ; 
 
theorem :: VECTSP11:34 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  "st" (Bool (Bool (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_vectsp_5 :::"/\"::: )  (Set  "("  ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_4 :::"(0)."::: )  (Set (Var "V1")))))))) ; 
 
theorem :: VECTSP11:35 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#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  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set (Var "V"))  ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: )  (Set   ($#k1_ranknull :::"ker"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" )) "," (Set   ($#k3_ranknull :::"im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ))))))) ; 
 
theorem :: VECTSP11:36 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_5 :::"Linear_Compl"::: )   "of" (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set (Var "f"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set (Var "I"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))))) ; 
 
theorem :: VECTSP11:37 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_5 :::"Linear_Compl"::: )   "of" (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ))  (Bool  "for" (Set (Var "fI")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "I")) "," (Set (Var "I"))  "st" (Bool (Bool (Set (Var "fI"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set (Var "I"))))) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Set (Var "fI"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v"))))) "holds"  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1"))))))))))) ; 
 
theorem :: VECTSP11:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1")) "st"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k6_matrlin2 :::"*"::: )  (Set (Var "h")) ")" )  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "L"))  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" )  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "n")) ")" ))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )  ($#k6_matrlin2 :::"*"::: )  (Set (Var "h")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "h"))  ($#k6_matrlin2 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_vectsp11 :::"|^"::: )  (Set (Var "i")) ")" )))  ")" )  ")" ))))))) ; 
 
theorem :: VECTSP11:39 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V1"))  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L2"))) & (Bool (Set (Var "L2")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "f")))) "holds"  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_5 :::"Linear_Compl"::: )   "of" (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L1")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" ))  (Bool  "for" (Set (Var "fI")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "I")) "," (Set (Var "I"))  "st" (Bool (Bool (Set (Var "fI"))  ($#r1_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k8_matrlin2 :::"|"::: )  (Set (Var "I"))))) "holds"  (Bool  "("  (Bool (Set (Var "fI")) "is"   ($#v1_vectsp11 :::"with_eigenvalues"::: )  ) & (Bool (Set (Var "L1")) "is" (Bool  "not"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "fI")))) & (Bool (Set (Var "L2")) "is"    ($#m1_vectsp11 :::"eigenvalue"::: )   "of" (Set (Var "fI"))) & (Bool (Set   ($#k2_vectsp11 :::"UnionKers"::: )  (Set  "(" (Set (Var "f"))  ($#k3_matrlin :::"+"::: )  (Set  "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "L2")) ")" )  ($#k4_matrlin :::"*"::: )  (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "V1")) ")" ) ")" ) ")" )) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "I")))  ")" ))))))) ; 
 
theorem :: VECTSP11:40 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "U")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "U")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "for" (Set (Var "L")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Set (Var "U"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) )) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "U")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "U"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "u"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )  ")" )))))) ; 
 
theorem :: VECTSP11:41 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V2"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k2_ranknull :::".:"::: )  (Set (Var "A"))))) "holds"  (Bool  "ex" (Set (Var "M")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))))))))) ; 
 
theorem :: VECTSP11:42 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V2"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_ranknull :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")) ")" )))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "B")) ")" )))))))) ; 
 
theorem :: VECTSP11:43 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set  "("  ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")) ")" )  ($#k8_subset_1 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")) ")" ) ")" )) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "Lf")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V2")) "st"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "Lf")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_ranknull :::".:"::: )  (Set  "(" (Set  "("  ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")) ")" )  ($#k8_subset_1 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")) ")" ) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Lf"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "F")) ")" ))) & (Bool  "("   "for" (Set (Var "v1")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")) ")" )  ($#k8_subset_1 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")) ")" )))) "holds"  (Bool (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Lf"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v1")) ")" )))  ")" )  ")" ))))))) ; 
 
theorem :: VECTSP11:44 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V1"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V1"))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_mod_2 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_ranknull :::".:"::: )  (Set (Var "B"))) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V2"))) & (Bool (Set (Set (Var "f"))  ($#k2_ranknull :::".:"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V2")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))))))) ;