:: MATRTOP1  semantic presentation begin  






































registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v1_partfun3 :::"positive-yielding"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set "F"  ($#k5_relat_1 :::"|"::: )  "Y") ->   ($#v1_partfun3 :::"positive-yielding"::: )   ; 
end; registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v2_partfun3 :::"negative-yielding"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set "F"  ($#k5_relat_1 :::"|"::: )  "Y") ->   ($#v2_partfun3 :::"negative-yielding"::: )   ; 
end; registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v3_partfun3 :::"nonpositive-yielding"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set "F"  ($#k5_relat_1 :::"|"::: )  "Y") ->   ($#v3_partfun3 :::"nonpositive-yielding"::: )   ; 
end; registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v4_partfun3 :::"nonnegative-yielding"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set "F"  ($#k5_relat_1 :::"|"::: )  "Y") ->   ($#v4_partfun3 :::"nonnegative-yielding"::: )   ; 
end; registrationlet "rf" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::); 
cluster (Set   ($#k1_partfun3 :::"sqrt"::: )  "rf") ->   ($#v1_finseq_1 :::"FinSequence-like"::: )   ; 
end; definitionlet "rf" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::); func  :::"@"::: "rf" ->   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) equals :: MATRTOP1:def 1 "rf"; end; 





:: deftheorem    defines :::"@"::: MATRTOP1:def 1 :  (Bool  "for" (Set (Var "rf")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_matrtop1 :::"@"::: )  (Set (Var "rf")))  ($#r1_hidden :::"="::: )  (Set (Var "rf")))); 
 definitionlet "p" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); func  :::"@"::: "p" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: MATRTOP1:def 2 "p"; end; 





:: deftheorem    defines :::"@"::: MATRTOP1:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"  (Bool (Set   ($#k2_matrtop1 :::"@"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))); 
 
theorem :: MATRTOP1:1 (Bool  "for" (Set (Var "rf1")) "," (Set (Var "rf2")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "rf1")) ")" )  ($#k3_fvsum_1 :::"+"::: )  (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "rf2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "rf1"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "rf2"))))) ; 
 
theorem :: MATRTOP1:2 (Bool  "for" (Set (Var "rf1")) "," (Set (Var "rf2")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_partfun3 :::"sqrt"::: )  (Set  "(" (Set (Var "rf1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "rf2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_partfun3 :::"sqrt"::: )  (Set (Var "rf1")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "("  ($#k1_partfun3 :::"sqrt"::: )  (Set (Var "rf2")) ")" )))) ; 
 
theorem :: MATRTOP1:3 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_partfun3 :::"sqrt"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "r")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: MATRTOP1:4 (Bool  "for" (Set (Var "rf")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_partfun3 :::"sqrt"::: )  (Set  "(" (Set (Var "rf"))  ($#k39_valued_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_euclid :::"abs"::: )  (Set (Var "rf"))))) ; 
 
theorem :: MATRTOP1:5 (Bool  "for" (Set (Var "rf")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "rf")) "is"   ($#v4_partfun3 :::"nonnegative-yielding"::: )  )) "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k16_rvsum_1 :::"Sum"::: )  (Set (Var "rf")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k1_partfun3 :::"sqrt"::: )  (Set (Var "rf")) ")" )))) ; 
 
theorem :: MATRTOP1:6 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) (Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" ))) ; 
 registrationlet "cf" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "cf"  ($#k1_finseq_3 :::"-"::: )  "X") ->   ($#v1_valued_0 :::"complex-valued"::: )   ; 
end; registrationlet "rf" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "rf"  ($#k1_finseq_3 :::"-"::: )  "X") ->   ($#v3_valued_0 :::"real-valued"::: )   ; 
end; registrationlet "cf" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSubsequence":::); 
cluster (Set   ($#k15_finseq_1 :::"Seq"::: )  "cf") ->   ($#v1_valued_0 :::"complex-valued"::: )   ; 
end; registrationlet "rf" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSubsequence":::); 
cluster (Set   ($#k15_finseq_1 :::"Seq"::: )  "rf") ->   ($#v3_valued_0 :::"real-valued"::: )   ; 
end; 
theorem :: MATRTOP1:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P"))))) "holds"  (Bool  "ex" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X")) ")" ) ")" ) "st" (Bool (Set (Set (Var "f1"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "Q")))))))) ; 
 
theorem :: MATRTOP1:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "cf")) "," (Set (Var "cf1")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "cf")) ")" )  "st" (Bool (Bool (Set (Var "cf1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "cf"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P"))))) "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "cf1"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "cf"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X")) ")" )))))) ; 
 
theorem :: MATRTOP1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "being"   ($#m1_hidden :::"FinSubsequence":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P"))))) "holds"  (Bool  "ex" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ) ")" ) ")" ) "st" (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "Q")))))))) ; 
 
theorem :: MATRTOP1:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "cf")) "," (Set (Var "cf1")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"FinSubsequence":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "cf")) ")" )  "st" (Bool (Bool (Set (Var "cf1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "cf"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P"))))) "holds"  (Bool (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "cf"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k16_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "cf1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ) ")" )))))) ; 
 
theorem :: MATRTOP1:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSubsequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "i"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k12_pnproc_1 :::"Shift"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k12_pnproc_1 :::"Shift"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y")) ")" )))))) ; 
 
theorem :: MATRTOP1:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"FinSequence":::) (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y")) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) "iff" (Bool (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ) ")" )))  ")" )  ")" )  ")" )))) ; 
 
theorem :: MATRTOP1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g1")) "," (Set (Var "f1")) "," (Set (Var "g2")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f1")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g2")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f2"))))) "holds"  (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "g1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g2")) ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "g1"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "("  ($#k15_finseq_1 :::"Seq"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "g2"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" ) ")" ))))) ; 
 
theorem :: MATRTOP1:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_finseq_3 :::"-"::: )  (Set (Var "X"))) "is"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "M"))  ($#k8_relat_1 :::"""::: )  (Set (Var "X")) ")" ) ")" )) "," (Set (Var "m")) "," (Set (Var "D"))))))) ; 
 
theorem :: MATRTOP1:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "M")) ")" )))) "holds"  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "(" (Set (Var "M"))  ($#k4_matrix11 :::"*"::: )  (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "i")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "F"))))))))) ; 
 
theorem :: MATRTOP1:16 (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")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "n"))) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set  "(" (Set (Var "A"))  ($#k8_matrlin :::"^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "m"))))))) ; 
 
theorem :: MATRTOP1:17 (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")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Set (Var "n"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "m"))) "," (Set (Var "K")) "st" (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set  "(" (Set (Var "A"))  ($#k1_matrix15 :::"^^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))))) ; 
 


















begin  definitionlet "n", "m" be   ($#m1_hidden :::"Nat":::); let "M" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); func  :::"Mx2Tran"::: "M" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "m" ")" ) means :: MATRTOP1:def 3 (Bool  "for" (Set (Var "f")) "being" "n"  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "(" (Set  "("  ($#k2_matrix15 :::"LineVec2Mx"::: )  (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "f")) ")" ) ")" )  ($#k4_matrix_3 :::"*"::: )  "M" ")" ) "," (Num 1) ")" ))) if (Bool "n"  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "for" (Set (Var "f")) "being" "n"  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "m" ")" )))); end; 







:: deftheorem    defines :::"Mx2Tran"::: MATRTOP1:def 3 :  (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"::: ) )  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")))) "iff" (Bool  "for" (Set (Var "f")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "(" (Set  "("  ($#k2_matrix15 :::"LineVec2Mx"::: )  (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "f")) ")" ) ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "M")) ")" ) "," (Num 1) ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")))) "iff" (Bool  "for" (Set (Var "f")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" ))))  ")" )  ")"   ")" )))); 
 registrationlet "n", "m" be   ($#m1_hidden :::"Nat":::); let "M" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  "M" ")" )  ($#k1_funct_1 :::"."::: )  "x") ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 

cluster (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  "M" ")" )  ($#k1_funct_1 :::"."::: )  "x") ->   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v3_valued_0 :::"real-valued"::: )   ; 
end; registrationlet "n", "m" be   ($#m1_hidden :::"Nat":::); let "M" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); let "f" be (Set (Const "n"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::); 
cluster (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  "M" ")" )  ($#k1_funct_1 :::"."::: )  "f") -> "m"  ($#v3_card_1 :::"-element"::: )   ; 
end; 
theorem :: MATRTOP1:18 (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being" (Set (Var "b3"))  ($#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 (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "f")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "i")) ")"  ")" )))))) ; 
 
theorem :: MATRTOP1:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k11_matrix13 :::"MX2FinS"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))) ; 
 
theorem :: MATRTOP1:20 (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"::: ) )  (Bool  "for" (Set (Var "Bn")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  (Bool  "for" (Set (Var "Bm")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set (Set (Var "m"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))  "st" (Bool (Bool (Set (Var "Bn"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_matrix13 :::"MX2FinS"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "Bm"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_matrix13 :::"MX2FinS"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "m")) ")"  ")" )))) "holds"  (Bool  "for" (Set (Var "M1")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bn"))) "," (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Bm"))) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set (Var "M1"))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")))  ($#r1_funct_2 :::"="::: )  (Set   ($#k4_matrlin2 :::"Mx2Tran"::: )   "(" (Set (Var "M1")) "," (Set (Var "Bn")) "," (Set (Var "Bm")) ")" ))))))) ; 
 
theorem :: MATRTOP1:21 (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 "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "M"))  ($#k4_matrix11 :::"*"::: )  (Set (Var "P")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P"))) "is" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ))))) ; 
 
theorem :: MATRTOP1:22 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "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"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f1"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f1")) ")" )  ($#k4_rvsum_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f2")) ")" )))))) ; 
 
theorem :: MATRTOP1:23 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (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"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k10_rvsum_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ))))))) ; 
 
theorem :: MATRTOP1:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "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"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f1")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f2")) ")" )))))) ; 
 
theorem :: MATRTOP1:25 (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 "M1")) "," (Set (Var "M2")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "M1"))  ($#k5_matrlin2 :::"+"::: )  (Set (Var "M2")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M1")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k4_rvsum_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: MATRTOP1:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (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 "r"))  ($#r1_hidden :::"="::: )  (Set (Var "R")))) "holds"  (Bool (Set (Set (Var "r"))  ($#k10_rvsum_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "R"))  ($#k2_matrix13 :::"*"::: )  (Set (Var "M")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f"))))))))) ; 
 
theorem :: MATRTOP1:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (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 (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "p1"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")) ")" )  ($#k1_algstr_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")) ")" )))))) ; 
 
theorem :: MATRTOP1:28 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (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 (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "p1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "p2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p2")) ")" )))))) ; 
 
theorem :: MATRTOP1:29 (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 (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" ))))) ; 
 
theorem :: MATRTOP1:30 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (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"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set  "(" (Set (Var "p"))  ($#k5_rusub_4 :::"+"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k5_rusub_4 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k2_ranknull :::".:"::: )  (Set (Var "A")) ")" ))))))) ; 
 
theorem :: MATRTOP1:31 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (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"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "m")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_ranknull :::"""::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k5_rusub_4 :::"+"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_rusub_4 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_ranknull :::"""::: )  (Set (Var "A")) ")" ))))))) ; 
 
theorem :: MATRTOP1:32 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "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_matrix_1 :::"Matrix":::) "of" (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A"))) "," (Set (Var "k")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "B")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrix_3 :::"*"::: )  (Set (Var "B")) ")" )))))) ; 
 
theorem :: MATRTOP1:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: MATRTOP1:34 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M1")) "," (Set (Var "M2")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M1")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M2"))))) "holds"  (Bool (Set (Var "M1"))  ($#r1_hidden :::"="::: )  (Set (Var "M2"))))) ; 
 
theorem :: MATRTOP1:35 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (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 "A")) "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_matrix_1 :::"Matrix":::) "of" (Set (Var "k")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "A"))  ($#k8_matrlin :::"^"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "k"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))) & (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "B"))  ($#k8_matrlin :::"^"::: )  (Set (Var "A")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "k"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f"))))  ")" ))))) ; 
 
theorem :: MATRTOP1:36 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (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 "A")) "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_matrix_1 :::"Matrix":::) "of" (Set (Var "k")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "g")) "being" (Set (Var "b3"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "A"))  ($#k8_matrlin :::"^"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k4_rvsum_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "B")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "g")) ")" )))))))) ; 
 
theorem :: MATRTOP1:37 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (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 "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "(" (Set (Var "A"))  ($#k1_matrix15 :::"^^"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "B")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ))))))) ; 
 
theorem :: MATRTOP1:38 (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"::: ) )  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "m")) ")"  ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k16_finseq_1 :::"|"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))))) ; 
 begin  
theorem :: MATRTOP1:39 (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"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: MATRTOP1:40 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")" ))) ; 
 
theorem :: MATRTOP1:41 (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  "("  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M"))) "is"   ($#v2_funct_2 :::"onto"::: )  ) "iff" (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "m")))  ")" ))) ; 
 
theorem :: MATRTOP1:42 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A"))) "is"   ($#v2_funct_2 :::"onto"::: )  ) "iff" (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")" ))) ; 
 
theorem :: MATRTOP1:43 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "A")) ")" )  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "B")))) "iff" (Bool (Set (Set (Var "A"))  ($#k5_matrix_6 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "B")))  ")" ))) ; 
 
theorem :: MATRTOP1:44 (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  "ex" (Set (Var "L")) "being" (Set (Var "b1"))  ($#v3_card_1 :::"-element"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "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 "L"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "("  ($#k2_matrtop1 :::"@"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "M")) "," (Set (Var "i")) ")"  ")" ) ")" ) ($#k12_euclid :::".|"::: ) ))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "L")) ")" )  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) )))  ")" )  ")" )))) ; 
 
theorem :: MATRTOP1:45 (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  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "f")) "being" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "L"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) )))  ")" )  ")" )))) ; 
 
theorem :: MATRTOP1:46 (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  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "f")) "being" (Set (Var "b2"))  ($#v3_card_1 :::"-element"::: )     ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "L"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) )))  ")" )  ")" )))) ; 
 
theorem :: MATRTOP1:47 (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   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M"))) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "K" be   ($#l6_algstr_0 :::"Field":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K")  ($#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_matrix_1 :::"tabular"::: )     ($#v1_matrix_6 :::"invertible"::: )    for    ($#m1_matrix_1 :::"Matrix"::: )   "of" "n" "," "n" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "K"); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "A" be   ($#v1_matrix_6 :::"invertible"::: )    ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); 
cluster (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  "A") ->   ($#v3_tops_2 :::"being_homeomorphism"::: )   ; 
end;