:: MATRTOP2  semantic presentation begin  

















theorem :: MATRTOP2:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))) "iff" (Bool (Set (Var "X")) "is"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n"))))  ")" ))) ; 
 
theorem :: MATRTOP2:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Lv")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  (Bool  "for" (Set (Var "Lr")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set (Var "Lr"))  ($#r1_funct_2 :::"="::: )  (Set (Var "Lv")))) "holds"  (Bool (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "Lr")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "Lv"))))))) ; 
 
theorem :: MATRTOP2:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "fr")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Fv")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  (Bool  "for" (Set (Var "fv")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" ) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set (Var "fr"))  ($#r1_funct_2 :::"="::: )  (Set (Var "fv"))) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "Fv")))) "holds"  (Bool (Set (Set (Var "fr"))  ($#k5_rlvect_2 :::"(#)"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fv"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "Fv"))))))))) ; 
 
theorem :: MATRTOP2:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Fv")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  "st" (Bool (Bool (Set (Var "Fv"))  ($#r1_hidden :::"="::: )  (Set (Var "F")))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set (Var "Fv"))))))) ; 
 
theorem :: MATRTOP2:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Lv")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  (Bool  "for" (Set (Var "Lr")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set (Var "Lr"))  ($#r1_funct_2 :::"="::: )  (Set (Var "Lv")))) "holds"  (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "Lr")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "Lv"))))))) ; 
 
theorem :: MATRTOP2:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  (Bool  "for" (Set (Var "Ar")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "Af"))  ($#r1_hidden :::"="::: )  (Set (Var "Ar")))) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "Ar")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "Af")) ")" )))))) ; 
 
theorem :: MATRTOP2:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  (Bool  "for" (Set (Var "Ar")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "Af"))  ($#r1_hidden :::"="::: )  (Set (Var "Ar")))) "holds"  (Bool  "("  (Bool (Set (Var "Af")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  ) "iff" (Bool (Set (Var "Ar")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )  ")" )))) ; 
 
theorem :: MATRTOP2:8 (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 "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "L"))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W")))) "is"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "W"))))))) ; 
 
theorem :: MATRTOP2:9 (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 "A")) "being"   ($#v1_vectsp_7 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L1")))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L2")))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L2"))))) "holds"  (Bool (Set (Var "L1"))  ($#r1_vectsp_6 :::"="::: )  (Set (Var "L2"))))))) ; 
 
theorem :: MATRTOP2:10 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "L"))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W")))) "is"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "W")))))) ; 
 
theorem :: MATRTOP2:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "U")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "U")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "W"))))) "holds"  (Bool  "("  (Bool (Set (Var "X")) "is"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "U"))) "iff" (Bool (Set (Var "X")) "is"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "W")))  ")" ))))) ; 
 
theorem :: MATRTOP2:12 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "U")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")))  (Bool  "for" (Set (Var "LU")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "U"))  (Bool  "for" (Set (Var "LW")) "being"    ($#m1_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "LU"))  ($#r1_funct_2 :::"="::: )  (Set (Var "LW")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "LU")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "LW")))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "LU")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "LW"))))  ")" )))))) ; 
 registrationlet "m" be   ($#m1_hidden :::"Nat":::); let "K" be   ($#l6_algstr_0 :::"Field":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Const "m"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set (Const "K")) ")" ); 
cluster (Set   ($#k1_vectsp_7 :::"Lin"::: )  "A") ->   ($#v1_matrlin :::"finite-dimensional"::: )   ; 
end; begin  
theorem :: MATRTOP2:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "M")) "is"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k9_matrix13 :::"lines"::: )  (Set (Var "M")) ")" ))))) ; 
 
theorem :: MATRTOP2:14 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "," (Set (Var "W")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Set (Var "T"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "T"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set  "(" (Set (Var "T"))  ($#k8_ranknull :::"@"::: )  (Set (Var "L")) ")" )))))))) ; 
 
theorem :: MATRTOP2:15 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "M"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "S"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "M"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "S")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrix13 :::"lines"::: )  (Set (Var "M"))))) "holds"  (Bool  "ex" (Set (Var "L")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set   ($#k9_matrix13 :::"lines"::: )  (Set (Var "M"))) "st"  (Bool  "("  (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "M"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "k")) ")"  ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" )))  ")" )  ")" )))))) ; 
 
theorem :: MATRTOP2:16 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v2_funct_1 :::"without_repeated_line"::: )  )) "holds"  (Bool  "ex" (Set (Var "L")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set   ($#k9_matrix13 :::"lines"::: )  (Set (Var "M"))) "st"  (Bool  "("  (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "M")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )  ")" ))))) ; 
 
theorem :: MATRTOP2:17 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k9_matrix13 :::"lines"::: )  (Set (Var "M")) ")" ))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) "holds"  (Bool  "for" (Set (Var "Mf")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k9_matrix13 :::"lines"::: )  (Set (Var "M")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "Mf"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "Mf"))  ($#k9_matrlin :::"|--"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))))))) ; 
 
theorem :: MATRTOP2:18 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k9_matrix13 :::"lines"::: )  (Set (Var "M")) ")" ) ")" ))))) ; 
 
theorem :: MATRTOP2:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#v2_funct_1 :::"one-to-one"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F"))) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "ex" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_matrix_6 :::"invertible"::: )  ) & (Bool (Set (Set (Var "M"))  ($#k17_finseq_1 :::"|"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "F")))  ")" )))) ; 
 
theorem :: MATRTOP2:20 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_matrix13 :::"MX2FinS"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "B"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")) ")" ) ")" ))) "iff" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k16_finseq_1 :::"|"::: )  (Set (Var "k")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )))  ")" )))) ; 
 
theorem :: MATRTOP2:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#v2_funct_1 :::"one-to-one"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F"))) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_matrix13 :::"MX2FinS"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v1_matrix_6 :::"invertible"::: )  ) & (Bool (Set (Set (Var "M"))  ($#k17_finseq_1 :::"|"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "B"))  ($#k17_finseq_1 :::"|"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")) ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ) ")" ))))))) ; 
 
theorem :: MATRTOP2:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_rlvect_3 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "B"))))) "holds"  (Bool  "ex" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_matrix_6 :::"invertible"::: )  ) & (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")) ")" )))  ")" )))) ; 
 begin  
theorem :: MATRTOP2:23 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlvect_3 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set (Var "A"))) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )))) ; 
 
theorem :: MATRTOP2:24 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set (Var "A"))) "is"   ($#v1_rlaffin1 :::"affinely-independent"::: )  )))) ; 
 
theorem :: MATRTOP2:25 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set (Var "A")) ")" ))) & (Bool  "("   "for" (Set (Var "f")) "being" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "v"))  ($#k5_rlaffin1 :::"|--"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "v")) ")" )  ($#k5_rlaffin1 :::"|--"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set (Var "A")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )))  ")" )  ")" ))))) ; 
 
theorem :: MATRTOP2:26 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlvect_3 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_ranknull :::"""::: )  (Set (Var "A"))) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )))) ; 
 
theorem :: MATRTOP2:27 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_ranknull :::"""::: )  (Set (Var "A"))) "is"   ($#v1_rlaffin1 :::"affinely-independent"::: )  )))) ;