:: MATRIX_3 semantic presentation begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n", "m" be ($#m1_hidden :::"Nat":::); func :::"0."::: "(" "K" "," "n" "," "m" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K" equals :: MATRIX_3:def 1 (Set "n" ($#k5_finseq_2 :::"|->"::: ) (Set "(" "m" ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) ")" )); end; :: deftheorem defines :::"0."::: MATRIX_3:def 1 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "m")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ))))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); func :::"-"::: "A" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIX_3:def 2 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "A")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "A")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "A"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "A" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-"::: MATRIX_3:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix_3 :::"-"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "b3")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" ))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A", "B" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); func "A" :::"+"::: "B" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIX_3:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "A")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "A")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "A"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "A" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" "B" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"+"::: MATRIX_3:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "b4")) ($#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")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" ))); theorem :: MATRIX_3: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 "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_3:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "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 (Set (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "A")))))) ; theorem :: MATRIX_3:3 (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 "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 (Set (Set "(" (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "B")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "C")) ")" ))))) ; theorem :: MATRIX_3: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 "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: MATRIX_3: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 "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k2_matrix_3 :::"-"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A", "B" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); assume (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Const "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "B")))) ; func "A" :::"*"::: "B" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIX_3:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "A")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "B")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) it))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "A" "," (Set (Var "i")) ")" ")" ) ($#k13_fvsum_1 :::""*""::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" "B" "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"*"::: MATRIX_3:def 4 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k13_fvsum_1 :::""*""::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "B")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" )))); definitionlet "n", "k", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "k")) "," (Set (Const "K")); let "B" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k1_matrix_1 :::"width"::: ) (Set (Const "A"))) "," (Set (Const "m")) "," (Set (Const "K")); :: original: :::"*"::: redefine func "A" :::"*"::: "B" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "A") "," (Set ($#k1_matrix_1 :::"width"::: ) "B") "," "K"; end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "a" :::"*"::: "M" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIX_3:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (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")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"*"::: MATRIX_3:def 5 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "M"))))) "holds" (Bool (Set (Set (Var "b4")) ($#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 "j")) ")" ")" ))) ")" ) ")" ) ")" ))))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "M" :::"*"::: "a" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" equals :: MATRIX_3:def 6 (Set "a" ($#k6_matrix_3 :::"*"::: ) "M"); end; :: deftheorem defines :::"*"::: MATRIX_3:def 6 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "M")) ($#k7_matrix_3 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "M"))))))); theorem :: MATRIX_3:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) ")" ))) ; theorem :: MATRIX_3:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "l")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_3:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "l")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "l")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "l")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_3:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "l")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "l")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_3:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; theorem :: MATRIX_3:12 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: MATRIX_3:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" )))) ; theorem :: MATRIX_3:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" )) "holds" (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" ))))) ; theorem :: MATRIX_3:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" )))) ; theorem :: MATRIX_3:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "implies" (Bool (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" )))) ; theorem :: MATRIX_3:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: MATRIX_3:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: MATRIX_3:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: MATRIX_3:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) ) ($#k4_matrix_3 :::"*"::: ) (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "b")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) )))) ; theorem :: MATRIX_3:21 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c1")) "," (Set (Var "d1")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c2")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k8_group_1 :::"*"::: ) (Set (Var "c2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "b2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k8_group_1 :::"*"::: ) (Set (Var "d2")) ")" ) ")" ) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set "(" (Set "(" (Set (Var "c1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d1")) ($#k8_group_1 :::"*"::: ) (Set (Var "c2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "c1")) ($#k8_group_1 :::"*"::: ) (Set (Var "b2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "d1")) ($#k8_group_1 :::"*"::: ) (Set (Var "d2")) ")" ) ")" ) ")" )))) ; theorem :: MATRIX_3:22 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_1 :::"@"::: ) ")" ))))) ; begin definitionlet "I", "J" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "I"))); let "Y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "J"))); :: original: :::"[:"::: redefine func :::"[:":::"X" "," "Y":::":]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "I" "," "J" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "I", "J", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set (Const "D")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "J")) "," (Set (Const "D")); :: original: :::"*"::: redefine func "G" :::"*"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "I" "," "J" ($#k2_zfmisc_1 :::":]"::: ) ) "," "D"; end; theorem :: MATRIX_3:23 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k8_matrix_3 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ")" ) ")" )))))))) ; theorem :: MATRIX_3:24 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" )))))))) ; theorem :: MATRIX_3:25 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" ))))))))) ; theorem :: MATRIX_3:26 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set (Var "g")) ")" ")" ) ")" ")" ) ")" )))))))) ; theorem :: MATRIX_3:27 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) "," (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "g")) ")" ")" ) ")" )))))))) ; theorem :: MATRIX_3:28 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set "(" (Set (Var "G")) ($#k9_matrix_3 :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "g")) ")" ")" ) ")" )))))))) ; theorem :: MATRIX_3:29 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "g")) ")" )))))))) ; theorem :: MATRIX_3:30 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set (Var "g")) ")" )))))))) ; theorem :: MATRIX_3:31 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" (Set "(" ($#k12_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "j")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) ($#k8_matrix_3 :::":]"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "y")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "g")) ")" )))))))) ; theorem :: MATRIX_3:32 (Bool "for" (Set (Var "D")) "," (Set (Var "I")) "," (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set (Var "J")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "I"))) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "J"))) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "J")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" (Set "(" ($#k12_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "j")) ")" ) ")" )) ")" ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k8_matrix_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k8_matrix_3 :::":]"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "Y")) "," (Set (Var "g")) ")" )))))))) ; theorem :: MATRIX_3:33 (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 ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "C")) ")" ))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); let "p" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Const "n"))); func :::"Path_matrix"::: "(" "p" "," "M" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" means :: MATRIX_3:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) "n") & (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"::: ) it)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Path_matrix"::: MATRIX_3:def 7 : (Bool "for" (Set (Var "n")) "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 "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," (Set (Var "M")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (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 "b5")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ) ")" ) ")" )))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); func :::"Path_product"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) "n" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") means :: MATRIX_3:def 8 (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) "n") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," "M" ")" ")" ) ")" ) "," (Set (Var "p")) ")" ))); end; :: deftheorem defines :::"Path_product"::: MATRIX_3:def 8 : (Bool "for" (Set (Var "n")) "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 "K")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," (Set (Var "M")) ")" ")" ) ")" ) "," (Set (Var "p")) ")" ))) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); func :::"Det"::: "M" -> ($#m1_subset_1 :::"Element":::) "of" "K" equals :: MATRIX_3:def 9 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) "n" ")" ) ")" ) "," (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) "M" ")" ) ")" ); end; :: deftheorem defines :::"Det"::: MATRIX_3:def 9 : (Bool "for" (Set (Var "n")) "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 "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "M")) ")" ) ")" ))))); theorem :: MATRIX_3:34 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); func :::"diagonal_of_Matrix"::: "M" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" means :: MATRIX_3:def 10 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) "n") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"diagonal_of_Matrix"::: MATRIX_3:def 10 : (Bool "for" (Set (Var "n")) "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 "K")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrix_3 :::"diagonal_of_Matrix"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" )) ")" ) ")" ) ")" )))));