:: MATRIXR2  semantic presentation begin  

















theorem :: MATRIXR2:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))) & (Bool (Set (Set (Var "x"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set (Var "y")))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: MATRIXR2:2 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))))))) ; 
 
theorem :: MATRIXR2:3 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )))))) ; 
 
theorem :: MATRIXR2:4 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: MATRIXR2:5 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "(" (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A"))))  ")" ))) ; 
 begin  
theorem :: MATRIXR2:6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "B"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )))  ")" )  ")" )) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A", "B" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"*"::: redefine func "A" :::"*"::: "B" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set   ($#k1_numbers :::"REAL"::: )  ); end; 
theorem :: MATRIXR2:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_matrixr1 :::"+"::: )  (Set  "(" (Set (Var "B"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: MATRIXR2:8 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k3_matrixr1 :::"+"::: )  (Set (Var "B")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: MATRIXR2:9 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr1 :::"-"::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:10 (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr1 :::"-"::: )  (Set (Var "A")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))))) ; 
 
theorem :: MATRIXR2:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k7_real_1 :::"+"::: )  (Set (Var "b")) ")" )  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k3_matrixr1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_real_1 :::"-"::: )  (Set (Var "b")) ")" )  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:14 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")) ")" ) ")"  ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")) ")" ) ")" ))))) ; 
 
theorem :: MATRIXR2:15 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "C")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_matrix_3 :::"-"::: )  (Set (Var "C")) ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_3 :::"-"::: )  (Set  "(" (Set (Var "C"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:16 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "C")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "B"))  ($#k1_matrix_4 :::"-"::: )  (Set (Var "C")) ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")) ")" )  ($#k1_matrix_4 :::"-"::: )  (Set  "(" (Set (Var "C"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:17 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" )  ($#k6_matrixr1 :::"*"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "C")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set  "(" (Set (Var "B"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "C")) ")" )))) ; 
 
theorem :: MATRIXR2:18 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")) ")" ) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_3 :::"0."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")) ")" ) "," (Set (Var "m")) ")" ))))) ; 
 
theorem :: MATRIXR2:19 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k2_matrix_3 :::"-"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrix_3 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: MATRIXR2:20 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "C")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set  "(" (Set (Var "B"))  ($#k1_matrix_4 :::"-"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "B")) ")" )  ($#k1_matrix_4 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: MATRIXR2:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "C"))  ($#k6_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "C"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set  "(" (Set (Var "C"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: MATRIXR2:22 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "C"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "B"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" )))  ")" )) "holds"  (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B"))))) ; 
 
theorem :: MATRIXR2:23 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x2"))))) "holds"  (Bool (Set   ($#k10_matrixr1 :::"LineVec2Mx"::: )  (Set  "(" (Set (Var "x1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_matrixr1 :::"LineVec2Mx"::: )  (Set (Var "x1")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set  "("  ($#k10_matrixr1 :::"LineVec2Mx"::: )  (Set (Var "x2")) ")" )))) ; 
 
theorem :: MATRIXR2:24 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x2")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k9_matrixr1 :::"ColVec2Mx"::: )  (Set  "(" (Set (Var "x1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_matrixr1 :::"ColVec2Mx"::: )  (Set (Var "x1")) ")" )  ($#k5_matrixr1 :::"-"::: )  (Set  "("  ($#k9_matrixr1 :::"ColVec2Mx"::: )  (Set (Var "x2")) ")" )))) ; 
 
theorem :: MATRIXR2:25 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k8_matrix_1 :::"Line"::: )   "(" (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "A")) "," (Set (Var "i")) ")"  ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "B")) "," (Set (Var "i")) ")"  ")" ))))) ; 
 
theorem :: MATRIXR2:26 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "A")) "," (Set (Var "i")) ")"  ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "B")) "," (Set (Var "i")) ")"  ")" ))))) ; 
 
theorem :: MATRIXR2:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "k")) "," (Set (Var "m")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "m")) "," (Set (Var "l")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" )  ($#k6_matrixr1 :::"*"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "B"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "C")) ")" ))))))) ; 
 
theorem :: MATRIXR2:28 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" )  ($#k1_matrixr2 :::"*"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set  "(" (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: MATRIXR2:29 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k5_matrix_1 :::"@"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "A")))))) ; 
 
theorem :: MATRIXR2:30 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" )  ($#k5_matrix_1 :::"@"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k1_matrixr2 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" ))))) ; 
 
theorem :: MATRIXR2:31 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr1 :::"-"::: )  (Set (Var "A")) ")" )  ($#k3_matrixr1 :::"+"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )))) ; 
 begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ); :: original: :::"MXR2MXF"::: redefine func  :::"MXR2MXF"::: "A" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); end; definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ); func  :::"Det"::: "A" ->   ($#m1_subset_1 :::"Real":::) equals :: MATRIXR2:def 1 (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k2_matrixr2 :::"MXR2MXF"::: )  "A" ")" )); end; 






:: deftheorem    defines :::"Det"::: MATRIXR2:def 1 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k2_matrixr2 :::"MXR2MXF"::: )  (Set (Var "A")) ")" ))))); 
 
theorem :: MATRIXR2:32 (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Num 2) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 2) ")"  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 2) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 1) ")"  ")" ) ")" )))) ; 
 
theorem :: MATRIXR2:33 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "s3")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) ($#k11_finseq_1 :::"*>"::: ) ) "is"   ($#v1_matrix_1 :::"tabular"::: )  ))) ; 
 
theorem :: MATRIXR2:34 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p2")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p3")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k11_finseq_1 :::"<*"::: ) (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#k11_finseq_1 :::"*>"::: ) ) "is"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Num 3) "," (Set (Var "n")) "," (Set (Var "D")))))) ; 
 
theorem :: MATRIXR2:35 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set  ($#k11_finseq_1 :::"<*"::: ) (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set  ($#k3_finseq_4 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) ($#k3_finseq_4 :::"*>"::: ) ) ($#k11_finseq_1 :::"*>"::: ) ) "is"   ($#m1_matrix_1 :::"Matrix":::) "of" (Num 3) "," (Set (Var "D"))))) ; 
 
theorem :: MATRIXR2:36 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))))))) ; 
 
theorem :: MATRIXR2:37 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Num 3) "," (Set (Var "D")) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k11_finseq_1 :::"<*"::: ) (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 2) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 3) ")"  ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 2) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 3) ")"  ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "," (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 2) ")"  ")" ) "," (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 3) ")"  ")" ) ($#k3_finseq_4 :::"*>"::: ) ) ($#k11_finseq_1 :::"*>"::: ) )))) ; 
 
theorem :: MATRIXR2:38 (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Num 3) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 2) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 3) ")"  ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 3) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 2) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 1) ")"  ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 1) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 3) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 2) ")"  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 2) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 3) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 1) ")"  ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 2) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 1) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 3) ")"  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 1) "," (Num 3) ")"  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 2) "," (Num 1) ")"  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k3_matrix_1 :::"*"::: )   "(" (Num 3) "," (Num 2) ")"  ")" ) ")" )))) ; 
 
theorem :: MATRIXR2:39 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )))) ; 
 
theorem :: MATRIXR2:40 (Bool (Set   ($#k12_matrix_2 :::"Permutations"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: MATRIXR2:41 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k6_numbers :::"0"::: )  ) "," (Set (Var "K")) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "K")))))) ; 
 
theorem :: MATRIXR2:42 (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set   ($#k6_numbers :::"0"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: MATRIXR2:43 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" )))))) ; 
 
theorem :: MATRIXR2:44 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrixr2 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" ))))) ; 
 
theorem :: MATRIXR2:45 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"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")) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k4_matrix_6 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_matrix_3 :::"Det"::: )  (Set (Var "A")) ")" )  ($#k8_group_1 :::"*"::: )  (Set  "("  ($#k12_matrix_3 :::"Det"::: )  (Set (Var "B")) ")" )))))) ; 
 
theorem :: MATRIXR2:46 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_matrixr2 :::"Det"::: )  (Set (Var "B")) ")" ))))) ; 
 begin  
theorem :: MATRIXR2:47 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "y")) ")" )  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:48 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: MATRIXR2:49 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k6_rvsum_1 :::"-"::: )  (Set (Var "x")) ")" )  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:50 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set  "("  ($#k6_rvsum_1 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: MATRIXR2:51 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set  "("  ($#k4_matrixr1 :::"-"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:52 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr1 :::"-"::: )  (Set (Var "A")) ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: MATRIXR2:53 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k10_rvsum_1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: MATRIXR2:54 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MATRIXR2:55 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k5_matrixr1 :::"-"::: )  (Set (Var "B")) ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "(" (Set (Var "B"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: MATRIXR2:56 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Set  "("  ($#k10_matrixr1 :::"LineVec2Mx"::: )  (Set (Var "x")) ")" )  ($#k6_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_matrixr1 :::"LineVec2Mx"::: )  (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MATRIXR2:57 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k12_matrixr1 :::"*"::: )  (Set (Var "B")))))) ; 
 
theorem :: MATRIXR2:58 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set  "("  ($#k9_matrixr1 :::"ColVec2Mx"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_matrixr1 :::"ColVec2Mx"::: )  (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: MATRIXR2:59 (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "B")))) & (Bool (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "B")) ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "B"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: MATRIXR2:60 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"    ($#m1_matrix_1 :::"Matrix"::: )   "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "(" (Set (Var "B"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "B"))  ($#k6_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "B")) "," (Set (Var "i")) ")"  ")" )  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))))))) ; 
 
theorem :: MATRIXR2:61 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "(" (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k8_matrix_1 :::"Line"::: )   "(" (Set (Var "B")) "," (Set (Var "i")) ")"  ")" )  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))))) ; 
 
theorem :: MATRIXR2:62 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "B")) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))))) ; 
 begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"1_Rmatrix"::: "n" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: MATRIXR2:def 2 (Set   ($#k2_matrixr1 :::"MXF2MXR"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," "n" ")"  ")" )); end; 





:: deftheorem    defines :::"1_Rmatrix"::: MATRIXR2:def 2 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrixr1 :::"MXF2MXR"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" )))); 
 
theorem :: MATRIXR2:63 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) ; 
 
theorem :: MATRIXR2:64 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k5_matrix_1 :::"@"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))) ; 
 
theorem :: MATRIXR2:65 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" )  ($#k3_matrixr1 :::"+"::: )  (Set  "("  ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" ))) ; 
 
theorem :: MATRIXR2:66 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k7_matrixr1 :::"*"::: )  (Set  "("  ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "m")) ")" )))) ; 
 
theorem :: MATRIXR2:67 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "A"))  ($#k4_matrix_3 :::"*"::: )  (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set (Var "A")) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:68 (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set (Var "K")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "A")) ")" ) ")"  ")" )  ($#k4_matrix_3 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:69 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set (Var "A"))))) "implies" (Bool (Set (Set (Var "A"))  ($#k6_matrixr1 :::"*"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")"  &  "("  (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "A"))))) "implies" (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "m")) ")" )  ($#k6_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")"   ")" ))) ; 
 
theorem :: MATRIXR2:70 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:71 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:72 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"0_Rmatrix"::: "n" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: MATRIXR2:def 3 (Set   ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" "n" "," "n" ")" ); end; 





:: deftheorem    defines :::"0_Rmatrix"::: MATRIXR2:def 3 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k5_matrixr2 :::"0_Rmatrix"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_matrixr1 :::"0_Rmatrix"::: )   "(" (Set (Var "n")) "," (Set (Var "n")) ")" ))); 
 
theorem :: MATRIXR2:73 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set  "("  ($#k5_matrixr2 :::"0_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 definitionlet "n", "i" be   ($#m1_hidden :::"Nat":::); func  :::"Base_FinSeq":::  "(" "n" "," "i" ")"  ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: MATRIXR2:def 4 (Set (Set  "(" "n"  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" "i" "," (Num 1) ")" ); end; 






:: deftheorem    defines :::"Base_FinSeq"::: MATRIXR2:def 4 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Num 1) ")" ))); 
 





theorem :: MATRIXR2:74 (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: MATRIXR2:75 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: MATRIXR2:76 (Bool  "for" (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 



theorem :: MATRIXR2:77 (Bool  "("  (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 1) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k4_matrix_2 :::"<*"::: ) (Num 1) ($#k4_matrix_2 :::"*>"::: ) )) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 2) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 2) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 3) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_finseq_4 :::"*>"::: ) )) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 3) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k3_finseq_4 :::"*>"::: ) )) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Num 3) "," (Num 3) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k3_finseq_4 :::"<*"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k3_finseq_4 :::"*>"::: ) ))  ")" ) ; 
 
theorem :: MATRIXR2:78 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")" )))) ; 
 begin  definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ); attr "A" is  :::"invertible":::  means :: MATRIXR2:def 5 (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  "A")  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  "n")) & (Bool (Set "A"  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  "n"))  ")" )); end; 





:: deftheorem    defines :::"invertible"::: MATRIXR2:def 5 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  ) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))  ")" ))  ")" ))); 
 definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ); assume 
(Bool (Set (Const "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )
 ; func  :::"Inv"::: "A" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set   ($#k1_numbers :::"REAL"::: )  ) means :: MATRIXR2:def 6 (Bool  "("  (Bool (Set it  ($#k1_matrixr2 :::"*"::: )  "A")  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  "n")) & (Bool (Set "A"  ($#k1_matrixr2 :::"*"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  "n"))  ")" ); end; 







:: deftheorem    defines :::"Inv"::: MATRIXR2:def 6 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))  ")" )  ")" )))); 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  "n") ->   ($#v1_matrixr2 :::"invertible"::: )   ; 
end; 
theorem :: MATRIXR2:79 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k7_matrixr2 :::"Inv"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))) ; 
 
theorem :: MATRIXR2:80 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Set (Var "B1"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B2")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set (Var "B1"))  ($#r1_hidden :::"="::: )  (Set (Var "B2"))) & (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )  ")" ))) ; 
 
theorem :: MATRIXR2:81 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")) ")" )  ($#k2_real_1 :::"""::: )  )))) ; 
 
theorem :: MATRIXR2:82 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool (Set   ($#k3_matrixr2 :::"Det"::: )  (Set (Var "A")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: MATRIXR2:83 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B"))) "is"   ($#v1_matrixr2 :::"invertible"::: )  ) & (Bool (Set   ($#k7_matrixr2 :::"Inv"::: )  (Set  "(" (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "B")) ")" )  ($#k1_matrixr2 :::"*"::: )  (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")) ")" )))  ")" ))) ; 
 
theorem :: MATRIXR2:84 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool (Set   ($#k7_matrixr2 :::"Inv"::: )  (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MATRIXR2:85 (Bool  "("  (Bool (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_matrixr2 :::"0_Rmatrix"::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ) ; 
 
theorem :: MATRIXR2:86 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: MATRIXR2:87 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  ) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")) ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: MATRIXR2:88 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set  "("  ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: MATRIXR2:89 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  ) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k12_matrixr1 :::"*"::: )  (Set  "("  ($#k7_matrixr2 :::"Inv"::: )  (Set (Var "A")) ")" )))  ")" )))) ; 
 
theorem :: MATRIXR2:90 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool  "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))))) ; 
 
theorem :: MATRIXR2:91 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  )) "holds"  (Bool  "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))))) ; 
 
theorem :: MATRIXR2:92 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "y"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set (Var "A")) "," (Set (Var "j")) ")"  ")" ) ($#k23_rvsum_1 :::")|"::: ) )))))) ; 
 
theorem :: MATRIXR2:93 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "st" (Bool (Set (Set (Var "B"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))))) ; 
 
theorem :: MATRIXR2:94 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A"))))))) ; 
 
theorem :: MATRIXR2:95 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_matrixr1 :::"*"::: )  (Set  "(" (Set (Var "A"))  ($#k5_matrix_1 :::"@"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x"))))))) ; 
 
theorem :: MATRIXR2:96 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  ) "st" (Bool (Set (Set (Var "A"))  ($#k1_matrixr2 :::"*"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_matrixr2 :::"1_Rmatrix"::: )  (Set (Var "n"))))))) ; 
 
theorem :: MATRIXR2:97 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "x2")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "A"))  ($#k11_matrixr1 :::"*"::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "x2"))  ($#k12_matrixr1 :::"*"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))  ")" )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_matrixr2 :::"invertible"::: )  ))) ;