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

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