let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
Minor M,i,j = Minor (M @ ),j,i
let K be Field; :: thesis: for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
Minor M,i,j = Minor (M @ ),j,i
let M be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n holds
Minor M,i,j = Minor (M @ ),j,i
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n implies Minor M,i,j = Minor (M @ ),j,i )
assume that
A1: i in Seg n and
A2: j in Seg n ; :: thesis: Minor M,i,j = Minor (M @ ),j,i
thus Minor M,i,j = Det ((Delete M,i,j) @ ) by MATRIXR2:43
.= Minor (M @ ),j,i by A1, A2, Th14 ; :: thesis: verum