:: MATRIX14 semantic presentation begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"0*"::: "(" "K" "," "n" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" equals :: MATRIX14:def 1 (Set "n" ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" )); end; :: deftheorem defines :::"0*"::: MATRIX14:def 1 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_matrix14 :::"0*"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"0*"::: redefine func :::"0*"::: "(" "K" "," "n" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: MATRIX14:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))))) ; theorem :: MATRIX14:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "x1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1")))))) ; theorem :: MATRIX14:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "x1")) ($#k7_fvsum_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1")))))) ; theorem :: MATRIX14:4 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )))) ; theorem :: MATRIX14:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x1")) ($#k7_fvsum_1 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )))) ; theorem :: MATRIX14:6 (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 "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: MATRIX14:7 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "x1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "y2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ))))) ; notationlet "K" be ($#l6_algstr_0 :::"Field":::); let "e1", "e2" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); synonym :::"|(":::"e1" "," "e2":::")|"::: for "e1" :::""*""::: "e2"; end; theorem :: MATRIX14:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) & (Bool (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))) ")" )))) ; theorem :: MATRIX14:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set (Var "y")) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k13_fvsum_1 :::")|"::: ) )))))) ; theorem :: MATRIX14:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k13_fvsum_1 :::")|"::: ) )))))) ; theorem :: MATRIX14:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y1")) ($#k13_fvsum_1 :::")|"::: ) ) ($#k1_algstr_0 :::"+"::: ) (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set (Var "y2")) ($#k13_fvsum_1 :::")|"::: ) )))))) ; theorem :: MATRIX14:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y2"))))) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set "(" (Set (Var "x1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "y2")) ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k13_fvsum_1 :::")|"::: ) ) ($#k1_algstr_0 :::"+"::: ) (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k13_fvsum_1 :::")|"::: ) ))))) ; theorem :: MATRIX14:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p1")) "," (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; notationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); synonym :::"Inv"::: "A" for "A" :::"~"::: ; end; begin theorem :: MATRIX14:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) & (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: MATRIX14:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) ")" ))) ; theorem :: MATRIX14:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "K")) "holds" (Bool (Set (Var "A")) "is" ($#v1_matrix_6 :::"invertible"::: ) ))) ; theorem :: MATRIX14:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "C")) ")" )))))) ; theorem :: MATRIX14:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_matrix_6 :::"~"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" ) ")" )))) ; theorem :: MATRIX14:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" )) ")" )))) ; theorem :: MATRIX14:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k2_matrix14 :::"0*"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; theorem :: MATRIX14:21 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set "(" ($#k2_matrix14 :::"0*"::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")) ")" ) ")" ")" ) "," (Set (Var "x")) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; theorem :: MATRIX14:22 (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 ($#k13_fvsum_1 :::"|("::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n", "i" be ($#m1_hidden :::"Nat":::); func :::"Base_FinSeq"::: "(" "K" "," "n" "," "i" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" equals :: MATRIX14:def 2 (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" "n" ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) ")" ) "," "i" "," (Set "(" ($#k5_struct_0 :::"1."::: ) "K" ")" ) ")" ); end; :: deftheorem defines :::"Base_FinSeq"::: MATRIX14:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) "," (Set (Var "i")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ")" )))); theorem :: MATRIX14:23 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: MATRIX14:24 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))))) ; theorem :: MATRIX14:25 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (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 :: MATRIX14:26 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" )))) ; theorem :: MATRIX14:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: MATRIX14:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))) ; theorem :: MATRIX14:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_funcop_1 :::"IFEQ"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ))) ")" )))) ; begin theorem :: MATRIX14:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ; theorem :: MATRIX14:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k5_matrix_1 :::"@"::: ) )) ")" )))) ; theorem :: MATRIX14:32 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: MATRIX14:33 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))) ; theorem :: MATRIX14:34 (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "x")) "," (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))))) ; theorem :: MATRIX14:35 (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set (Var "x")) "," (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) ")" )))) ; theorem :: MATRIX14:36 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k13_fvsum_1 :::"|("::: ) (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "m")) "," (Set (Var "i")) ")" ")" ) ($#k13_fvsum_1 :::")|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))))) ; theorem :: MATRIX14:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "P")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" )) ")" ) & (Bool (Set (Set (Var "Q")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "Q")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k5_matrix_6 :::"~"::: ) )) ")" ))))) ; theorem :: MATRIX14:38 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "P")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "P")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_algstr_0 :::"""::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix14 :::"Base_FinSeq"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i")) ")" )) ")" )) "holds" (Bool (Set (Var "P")) "is" ($#v1_matrix_6 :::"invertible"::: ) ))))) ; theorem :: MATRIX14:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "P")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "P")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "P")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))))) ; theorem :: MATRIX14:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))))) ; theorem :: MATRIX14:41 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "P")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "Q")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "Q")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "Q")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "Q")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))))) ; begin theorem :: MATRIX14:42 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "D")) "holds" (Bool (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "D")))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i0" be ($#m1_hidden :::"Nat":::); func :::"SwapDiagonal"::: "(" "K" "," "n" "," "i0" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K" equals :: MATRIX14:def 3 (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" "K" "," "n" ")" ")" ) "," (Num 1) "," "i0" ")" ); end; :: deftheorem defines :::"SwapDiagonal"::: MATRIX14:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i0")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_7 :::"Swap"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) "," (Num 1) "," (Set (Var "i0")) ")" ))))); theorem :: MATRIX14:43 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i0")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i0"))) & (Bool (Set (Var "i0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "i0")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) ")" ) ")" )) "implies" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (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 (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" ) ")" ")" )))))) ; theorem :: MATRIX14:44 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Num 1) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))))))) ; theorem :: MATRIX14:45 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Num 1) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: MATRIX14:46 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "i0")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (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 (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ))))) ; theorem :: MATRIX14:47 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i0"))) & (Bool (Set (Var "i0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "i0")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) ")" ) "or" (Bool "(" (Bool (Bool "not" (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Var "i0")))) ")" ) ")" )) "implies" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (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 (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ")" ) ")" ")" ) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ))))) ; theorem :: MATRIX14:48 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i0"))) & (Bool (Set (Var "i0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i0")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i0")) "," (Set (Var "j")) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i0"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ) ")" ))))) ; theorem :: MATRIX14:49 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i0"))) & (Bool (Set (Var "i0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" )) ")" )))) ; theorem :: MATRIX14:50 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i0"))) & (Bool (Set (Var "i0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "i0")) ")" ))))) ; theorem :: MATRIX14:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "j0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j0"))) & (Bool (Set (Var "j0")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "j0")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" )) & (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "j0")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j0")) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "j0"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set "(" ($#k4_matrix14 :::"SwapDiagonal"::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "j0")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" ) ")" ))))) ; theorem :: MATRIX14:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))) ; begin theorem :: MATRIX14:53 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set "(" (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "C")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) ")" ))))) ; theorem :: MATRIX14:54 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "B2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )))))) ; theorem :: MATRIX14:55 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool "ex" (Set (Var "B1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Set (Set (Var "B1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "iff" (Bool "ex" (Set (Var "B2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) ")" )))) ; theorem :: MATRIX14:56 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) ")" )))) ;