:: MATRIX12 semantic presentation begin definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); func :::"InterchangeLine"::: "(" "M" "," "l" "," "k" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" "k" "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) "k")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" "l" "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "l") & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "k")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"InterchangeLine"::: MATRIX12:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b7")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix12 :::"InterchangeLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "l")) "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" )))))); theorem :: MATRIX12:1 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX12:2 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix12 :::"InterchangeLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" )) ")" ")" ))))) ; theorem :: MATRIX12:3 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" )))))))) ; definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func :::"ScalarXLine"::: "(" "M" "," "l" "," "a" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 2 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "a" ($#k8_group_1 :::"*"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" "l" "," (Set (Var "j")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"ScalarXLine"::: MATRIX12:def 2 : (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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b7")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix12 :::"ScalarXLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "l")) "," (Set (Var "j")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))))); theorem :: MATRIX12:4 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix12 :::"ScalarXLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "a")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" )) ")" ")" ))))) ; definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); assume (Bool (Set (Const "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "M")))) ; func :::"RlineXScalar"::: "(" "M" "," "l" "," "k" "," "a" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "a" ($#k8_group_1 :::"*"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" "k" "," (Set (Var "j")) ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" "l" "," (Set (Var "j")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"RlineXScalar"::: MATRIX12:def 3 : (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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "b8")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix12 :::"RlineXScalar"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b8"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b8")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "l")) "," (Set (Var "j")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b8")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))))); theorem :: MATRIX12:5 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix12 :::"RlineXScalar"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" )) ")" ")" ))))) ; notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); synonym :::"ILine"::: "(" "M" "," "l" "," "k" ")" for :::"InterchangeLine"::: "(" "M" "," "l" "," "k" ")" ; end; notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); synonym :::"SXLine"::: "(" "M" "," "l" "," "a" ")" for :::"ScalarXLine"::: "(" "M" "," "l" "," "a" ")" ; end; notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); synonym :::"RLineXS"::: "(" "M" "," "l" "," "k" "," "a" ")" for :::"RlineXScalar"::: "(" "M" "," "l" "," "k" "," "a" ")" ; end; theorem :: MATRIX12:6 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_matrix12 :::"ILine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ))))) ; theorem :: MATRIX12:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k2_matrix12 :::"SXLine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "a")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix12 :::"SXLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "a")) ")" ))))))) ; theorem :: MATRIX12:8 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" )))))) ; theorem :: MATRIX12:9 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: MATRIX12:10 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) "," (Set (Var "l")) ")" ))))) ; theorem :: MATRIX12:11 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set "(" ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: MATRIX12:12 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k1_matrix12 :::"ILine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix12 :::"ILine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" )) ")" ))) ; theorem :: MATRIX12:13 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "holds" (Bool "(" (Bool (Set ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" )) ")" )))) ; theorem :: MATRIX12:14 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool "(" (Bool (Set ($#k2_matrix12 :::"SXLine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "a")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k2_matrix12 :::"SXLine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "a")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix12 :::"SXLine"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" ) ")" )) ")" )))) ; definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); assume that (Bool (Set (Const "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")) ")" ))) and (Bool (Set (Const "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")) ")" ))) and (Bool (Set (Const "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool (Set (Const "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"InterchangeCol"::: "(" "M" "," "l" "," "k" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," "k" ")" )) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) "k")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," "l" ")" )) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) "l") & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) "k")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"InterchangeCol"::: MATRIX12:def 4 : (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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix12 :::"InterchangeCol"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" )) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "l")) ")" )) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" )))))); definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); assume that (Bool (Set (Const "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")) ")" ))) and (Bool (Set (Const "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool (Set (Const "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"ScalarXCol"::: "(" "M" "," "l" "," "a" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "a" ($#k8_group_1 :::"*"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," "l" ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"ScalarXCol"::: MATRIX12:def 5 : (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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix12 :::"ScalarXCol"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "l")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))))); definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); assume that (Bool (Set (Const "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")) ")" ))) and (Bool (Set (Const "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Const "M")) ")" ))) and (Bool (Set (Const "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool (Set (Const "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"RcolXScalar"::: "(" "M" "," "l" "," "k" "," "a" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" means :: MATRIX12:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "M" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "a" ($#k8_group_1 :::"*"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," "k" ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," "l" ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"RcolXScalar"::: MATRIX12:def 6 : (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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b8")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix12 :::"RcolXScalar"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b8"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b8")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "l")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b8")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))))); notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); synonym :::"ICol"::: "(" "M" "," "l" "," "k" ")" for :::"InterchangeCol"::: "(" "M" "," "l" "," "k" ")" ; end; notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); synonym :::"SXCol"::: "(" "M" "," "l" "," "a" ")" for :::"ScalarXCol"::: "(" "M" "," "l" "," "a" ")" ; end; notationlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "l", "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); synonym :::"RColXS"::: "(" "M" "," "l" "," "k" "," "a" ")" for :::"RcolXScalar"::: "(" "M" "," "l" "," "k" "," "a" ")" ; end; theorem :: MATRIX12:15 (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_matrix12 :::"ILine"::: ) "(" (Set (Var "M1")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix12 :::"ICol"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ))))) ; theorem :: MATRIX12:16 (Bool "for" (Set (Var "l")) "," (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_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_matrix12 :::"SXLine"::: ) "(" (Set (Var "M1")) "," (Set (Var "l")) "," (Set (Var "a")) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix12 :::"SXCol"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "a")) ")" )))))) ; theorem :: MATRIX12:17 (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "," (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_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_matrix12 :::"RLineXS"::: ) "(" (Set (Var "M1")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix12 :::"RColXS"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" )))))) ; theorem :: MATRIX12:18 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k4_matrix12 :::"ICol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix12 :::"ICol"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "k")) ")" ))))) ; theorem :: MATRIX12:19 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k5_matrix12 :::"SXCol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix12 :::"SXCol"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "a")) ")" )))))) ; theorem :: MATRIX12:20 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k6_matrix12 :::"RColXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix12 :::"RColXS"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" )))))) ; theorem :: MATRIX12:21 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_matrix12 :::"ICol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix12 :::"ICol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) ")" )))) ; theorem :: MATRIX12:22 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_matrix12 :::"RColXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set (Var "a")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix12 :::"RColXS"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "k")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: MATRIX12:23 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_matrix12 :::"SXCol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set (Var "a")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix12 :::"SXCol"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) ")" ) ")" ))))) ;