:: MATRIX15 semantic presentation begin theorem :: MATRIX15:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "," (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 (Set (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: MATRIX15:2 (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")) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")))) ")" )))) ; theorem :: MATRIX15:3 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "h")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "h")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "w")) ")" ))))) ; theorem :: MATRIX15:4 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "g")) ")" )))))) ; theorem :: MATRIX15:5 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p1"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p2"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "f2")))))) ; theorem :: MATRIX15:6 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (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 "f")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: MATRIX15:7 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (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"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "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 "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" )))))) ; theorem :: MATRIX15:8 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i"))))) ; theorem :: MATRIX15:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "Bx")) "," (Set (Var "By")) "," (Set (Var "Cx")) "," (Set (Var "Cy")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Bx")) "," (Set (Var "By")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Cx")) "," (Set (Var "Cy")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Bx"))) "," (Set ($#k5_card_1 :::"card"::: ) (Set (Var "By"))) "," (Set (Var "D")) (Bool "for" (Set (Var "C")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Cx"))) "," (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Cy"))) "," (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "bi")) "," (Set (Var "bj")) "," (Set (Var "ci")) "," (Set (Var "cj")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Bx")) "," (Set (Var "By")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Cx")) "," (Set (Var "Cy")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "bi")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "Bx")) ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "bj")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "By")) ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "ci")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "Cx")) ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "cj")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "Cy")) ")" ) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set (Var "B")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "bi")) "," (Set (Var "bj")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "ci")) "," (Set (Var "cj")) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) "," (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "M")) "," (Set (Var "Bx")) "," (Set (Var "By")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "M")) "," (Set (Var "Cx")) "," (Set (Var "Cy")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (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 (Set "(" ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Bx")) "," (Set (Var "By")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Cx")) "," (Set (Var "Cy")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))) "holds" (Bool (Set (Set (Var "M")) ($#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 :: MATRIX15:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "Q9")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "P")) "," (Set (Var "Q9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "P")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "Q")))) & (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 (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "Q9"))) & (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "Q9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Q9")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "Q")) ")" ")" ))))))) ; theorem :: MATRIX15:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" )) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" )))))) ; theorem :: MATRIX15:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" )) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set (Var "N")) ")" ")" )))))) ; theorem :: MATRIX15:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "U")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "U")))) "holds" (Bool (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" (Set "(" (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "U"))))))))) ; theorem :: MATRIX15:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "U")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool "(" "not" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) "or" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )) "holds" (Bool (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" (Set "(" (Set (Var "U")) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "u")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "U"))))))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n", "m", "k" be ($#m1_hidden :::"Nat":::); let "A" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "D")); let "B" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "k")) "," (Set (Const "D")); :: original: :::"^^"::: redefine func "A" :::"^^"::: "B" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) "A" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) "B" ")" )) "," "D"; end; theorem :: MATRIX15:15 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ")" )))))))) ; theorem :: MATRIX15:16 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ))))))) ; theorem :: MATRIX15:17 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ))))))) ; theorem :: MATRIX15:18 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "pA")) "," (Set (Var "pB")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pA"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pB"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k3_matrix11 :::"ReplaceLine"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) "," (Set "(" (Set (Var "pA")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "pB")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_matrix11 :::"ReplaceLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "pA")) ")" ")" ) ($#k1_matrix15 :::"^^"::: ) (Set "(" ($#k3_matrix11 :::"ReplaceLine"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) "," (Set (Var "pB")) ")" ")" )))))))) ; theorem :: MATRIX15:19 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set "(" (Set (Var "A")) ($#k1_matrix15 :::"^^"::: ) (Set (Var "B")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ))))) ; theorem :: MATRIX15:20 (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"))))) "holds" (Bool "(" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" ))) ")" ))) ; theorem :: MATRIX15:21 (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATRIX15: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 ($#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_xboole_0 :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k7_matrlin :::"^^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ))) ; theorem :: MATRIX15:23 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (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 (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) "," (Set (Var "m")) ")" ))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" )))))) ; theorem :: MATRIX15:24 (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 ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))))) "holds" (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"LineVec2Mx"::: "b" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Num 1) "," (Set ($#k3_finseq_1 :::"len"::: ) "b") "," "D" equals :: MATRIX15:def 1 (Set ($#k10_laplace :::"<*"::: ) "b" ($#k10_laplace :::"*>"::: ) ); func :::"ColVec2Mx"::: "b" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k3_finseq_1 :::"len"::: ) "b") "," (Num 1) "," "D" equals :: MATRIX15:def 2 (Set (Set ($#k10_laplace :::"<*"::: ) "b" ($#k10_laplace :::"*>"::: ) ) ($#k4_matrix_1 :::"@"::: ) ); end; :: deftheorem defines :::"LineVec2Mx"::: MATRIX15:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k10_laplace :::"<*"::: ) (Set (Var "b")) ($#k10_laplace :::"*>"::: ) )))); :: deftheorem defines :::"ColVec2Mx"::: MATRIX15:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k10_laplace :::"<*"::: ) (Set (Var "b")) ($#k10_laplace :::"*>"::: ) ) ($#k4_matrix_1 :::"@"::: ) )))); theorem :: MATRIX15:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "bD")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "MD")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "MD")) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set (Var "bD")))) "iff" (Bool "(" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MD")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "bD"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MD"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: MATRIX15:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "bD")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "MD")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MD"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "bD"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "MD")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "bD")))) "iff" (Bool "(" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "MD")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "bD"))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MD"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: MATRIX15:27 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set (Var "f")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "f")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MATRIX15:28 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set "(" (Set (Var "f")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MATRIX15:29 (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 "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "f")) ")" )))))) ; theorem :: MATRIX15:30 (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 "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "f")) ")" )))))) ; theorem :: MATRIX15:31 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Num 1) "," (Set (Var "k")) ")" )))) ; theorem :: MATRIX15:32 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "k")) "," (Num 1) ")" )))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A", "B" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); func :::"Solutions_of"::: "(" "A" "," "B" ")" -> ($#m1_hidden :::"set"::: ) equals :: MATRIX15:def 3 "{" (Set (Var "X")) where X "is" ($#m2_finseq_1 :::"Matrix":::) "of" "K" : (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "A")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "B")) & (Bool (Set "A" ($#k4_matrix_3 :::"*"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "B") ")" ) "}" ; end; :: deftheorem defines :::"Solutions_of"::: MATRIX15:def 3 : (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")) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) : (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) "}" ))); theorem :: MATRIX15:33 (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 (Bool "not" (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))))) ; theorem :: MATRIX15:34 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "X")) ")" ))) & (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "X")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "X")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; theorem :: MATRIX15:35 (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")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) ")" )) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) ")" )) ")" )))) ; theorem :: MATRIX15:36 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: MATRIX15:37 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "X2")) "," (Set (Var "B2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" )) & (Bool (Set (Var "X2")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B2")) ")" )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B2"))))) "holds" (Bool (Set (Set (Var "X1")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "X2"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "B1")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "B2")) ")" ) ")" )))) ; theorem :: MATRIX15:38 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "X")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A9")) "," (Set (Var "B9")) ")" ))) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" ")" ) ")" )))))))) ; theorem :: MATRIX15:39 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "X")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A9")) "," (Set (Var "B9")) ")" )) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" ) ")" )))))))) ; theorem :: MATRIX15:40 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A9")) "," (Set (Var "B9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" ) ")" ))))))) ; theorem :: MATRIX15:41 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; theorem :: MATRIX15:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (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")) (Bool "for" (Set (Var "nt")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "nt"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "nt")) "," (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_matrix13 :::"Segm"::: ) "(" (Set (Var "B")) "," (Set (Var "nt")) "," (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ")" ")" ) ")" )))))) ; theorem :: MATRIX15:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (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")) (Bool "for" (Set (Var "nt")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "nt"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "nt")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" ) ")" )) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "nt")) "," (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k1_matrix13 :::"Segm"::: ) "(" (Set (Var "B")) "," (Set (Var "nt")) "," (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ")" ")" ) ")" )))))) ; theorem :: MATRIX15:44 (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")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "N")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "B")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ) ")" ")" ) ")" ))))) ; theorem :: MATRIX15:45 (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")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "N")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N"))))) "holds" (Bool "(" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" ) ")" )) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "B")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ) ")" ")" ) ")" ))))) ; theorem :: MATRIX15:46 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (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 (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ")" ) ")" ))))) ; theorem :: MATRIX15:47 (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")) (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 "A")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")))) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "B")) "," (Set (Var "i")) ")" ")" ) ")" ))))) ; theorem :: MATRIX15:48 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "K")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_matrix11 :::"*"::: ) (Set (Var "P")) ")" ) "," (Set "(" (Set (Var "B")) ($#k4_matrix11 :::"*"::: ) (Set (Var "P")) ")" ) ")" )) & "(" (Bool (Bool (Set (Var "P")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "implies" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_matrix11 :::"*"::: ) (Set (Var "P")) ")" ) "," (Set "(" (Set (Var "B")) ($#k4_matrix11 :::"*"::: ) (Set (Var "P")) ")" ) ")" )) ")" ")" )))))) ; theorem :: MATRIX15:49 (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")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "MVectors")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "MVectors")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "MVectors")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix_3 :::"-"::: ) (Set "(" (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N")) ")" ) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ")" ))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "K")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l")))) "or" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ))) & (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MVectors")) "," (Set (Var "j")) ")" )) ")" )) "or" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "l")) ")" ")" ) ")" ))) ")" ) ")" )))))) ; theorem :: MATRIX15:50 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "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")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "l")) "," (Set (Var "K")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "X")) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) "," (Set (Var "l")) ")" )) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "X")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" ))))))) ; theorem :: MATRIX15:51 (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 ($#k1_xboole_0 :::"0"::: ) ) "," (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix13 :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_matrix13 :::"}"::: ) )))))) ; theorem :: MATRIX15:52 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "B")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: MATRIX15:53 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (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 "k")) "," (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set (Var "x")) "is" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "K")))))))) ; theorem :: MATRIX15:54 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "K")) : (Bool verum) "}" ))) ; theorem :: MATRIX15:55 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ")" ) "," (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )))) ; theorem :: MATRIX15:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ")" ) "," (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix13 :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_matrix13 :::"}"::: ) )))) ; begin scheme :: MATRIX15:sch 1 GAUSS1{ F1() -> ($#l6_algstr_0 :::"Field":::), F2() -> ($#m1_hidden :::"Nat":::), F3() -> ($#m1_hidden :::"Nat":::), F4() -> ($#m1_hidden :::"Nat":::), F5() -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ), F6() -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ), F7( ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ) "," ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::) "," ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" )) -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" )(Bool "ex" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" )(Bool "ex" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set F3 "(" ")" ))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A9")))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N")))) & (Bool P1[(Set (Var "A9")) "," (Set (Var "B9"))]) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A9")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" ) ")" ) "," (Set (Var "N")) ")" ) "is" ($#v2_matrix_1 :::"diagonal"::: ) ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" )))) "holds" (Bool (Set (Set (Var "A9")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "N")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ))) ")" ) & (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 "A9")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A9")) ")" ))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "N")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "A9")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ))) ")" ) ")" )))) provided (Bool P1[(Set F5 "(" ")" ) "," (Set F6 "(" ")" )]) and (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "A9")) "," (Set (Var "B9"))])) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A9"))))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set F7 "(" (Set (Var "B9")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "a")) ")" )]))))) proof end; scheme :: MATRIX15:sch 2 GAUSS2{ F1() -> ($#l6_algstr_0 :::"Field":::), F2() -> ($#m1_hidden :::"Nat":::), F3() -> ($#m1_hidden :::"Nat":::), F4() -> ($#m1_hidden :::"Nat":::), F5() -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ), F6() -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ), F7( ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ) "," ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::) "," ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" )) -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" )(Bool "ex" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" )(Bool "ex" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set F3 "(" ")" ))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A9")))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N")))) & (Bool P1[(Set (Var "A9")) "," (Set (Var "B9"))]) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A9")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" ) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set F1 "(" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" ) ")" )) & (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 "A9")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F3 "(" ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "N")) ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A9")) ")" ))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k5_matrix13 :::"Sgm"::: ) (Set (Var "N")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "A9")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set F1 "(" ")" ))) ")" ) ")" )))) provided (Bool P1[(Set F5 "(" ")" ) "," (Set F6 "(" ")" )]) and (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "," (Set F1 "(" ")" ) (Bool "for" (Set (Var "B9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set F2 "(" ")" ) "," (Set F4 "(" ")" ) "," (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "A9")) "," (Set (Var "B9"))])) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A9")))) & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set F1 "(" ")" ) ")" ))) ")" ) "holds" (Bool P1[(Set ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ) "," (Set F7 "(" (Set (Var "B9")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "a")) ")" )]))))) proof end; begin theorem :: MATRIX15:57 (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 (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool "(" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k7_matrlin :::"^^"::: ) (Set (Var "B")) ")" ))) "iff" (Bool (Bool "not" (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "b" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); func :::"Solutions_of"::: "(" "A" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: MATRIX15:def 4 "{" (Set (Var "f")) where f "is" ($#m2_finseq_1 :::"FinSequence":::) "of" "K" : (Bool (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" "A" "," (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) "b" ")" ) ")" )) "}" ; end; :: deftheorem defines :::"Solutions_of"::: MATRIX15:def 4 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k5_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) : (Bool (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "b")) ")" ) ")" )) "}" )))); theorem :: MATRIX15:58 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "b")) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")))) ")" )))))) ; theorem :: MATRIX15:59 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b")) "," (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k3_matrix15 :::"ColVec2Mx"::: ) (Set (Var "b")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "b" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); :: original: :::"Solutions_of"::: redefine func :::"Solutions_of"::: "(" "A" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) "A" ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) "K" ")" ); end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k5_matrix15 :::"Solutions_of"::: ) "(" "A" "," (Set "(" "k" ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) ")" ) ")" ) -> ($#v1_vectsp_4 :::"linearly-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) "A" ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) "K" ")" ); end; theorem :: MATRIX15:60 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))))) ; theorem :: MATRIX15:61 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool "(" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) "or" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" )) "holds" (Bool "not" (Bool (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); assume "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Const "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ; func :::"Space_of_Solutions_of"::: "A" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) "A" ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) "K") means :: MATRIX15:def 5 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" "A" "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "A" ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Space_of_Solutions_of"::: MATRIX15:def 5 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ")" )) ")" )))); theorem :: MATRIX15:62 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k6_matrix15 :::"Solutions_of"::: ) "(" (Set (Var "A")) "," (Set (Var "b")) ")" ) "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A"))))))) ; theorem :: MATRIX15:63 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K")))))) ; theorem :: MATRIX15:64 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )))) ; theorem :: MATRIX15:65 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A9")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ) "holds" (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A9"))) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A9")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" )))))))) ; theorem :: MATRIX15:66 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "N")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" )) "holds" (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set (Var "N")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ) ")" ")" )))))) ; theorem :: MATRIX15:67 (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")) (Bool "for" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "MVectors")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) "," (Set (Var "m")) "," (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "MVectors")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "MVectors")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix_3 :::"-"::: ) (Set "(" (Set "(" ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "N")) ")" ) ")" ")" ) ($#k4_matrix_1 :::"@"::: ) ")" ))) & (Bool (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" ($#k9_matrix13 :::"lines"::: ) (Set (Var "MVectors")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A")))) ")" )))))) ; theorem :: MATRIX15:68 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A")) ")" ))))) ; theorem :: MATRIX15:69 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v2_funct_1 :::"without_repeated_line"::: ) ) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M")))) & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ) "holds" (Bool (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" ($#k9_matrix13 :::"lines"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" ($#k9_matrix13 :::"lines"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" ) ")" )))))))) ; theorem :: MATRIX15:70 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "m")) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))) (Bool "ex" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W"))) "," (Set (Var "m")) "," (Set (Var "K"))(Bool "ex" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N")))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ")" )) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")))) & (Bool (Set ($#k9_matrix13 :::"lines"::: ) (Set (Var "A"))) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "W"))) ")" )))))) ; theorem :: MATRIX15:71 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "m")) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))) "st" (Bool (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" )) "," (Set (Var "m")) "," (Set (Var "K"))(Bool "ex" (Set (Var "N")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v1_setfam_1 :::"without_zero"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ))) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ")" ) ")" ) "," (Set (Var "N")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W")) ")" ) ")" ) ")" )) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "A")))) ")" )))))) ; theorem :: MATRIX15:72 (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 (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "B"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ))))) ; theorem :: MATRIX15:73 (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 "(" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A")))) & (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "B")))) ")" ))) ; theorem :: MATRIX15:74 (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 "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))) & "(" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ))))))) ; theorem :: MATRIX15:75 (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 "n")) "," (Set (Var "K")) (Bool "for" (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 ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "B")))))))) ; theorem :: MATRIX15:76 (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 "n")) "," (Set (Var "K")) (Bool "for" (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 ($#k1_matrix_1 :::"width"::: ) (Set (Var "B")))) & (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" (Set (Var "B")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "B")))))))) ;