let K be Field; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm M,P,Q) = Det (EqSegm (M @ ),Q,P)
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm M,P,Q) = Det (EqSegm (M @ ),Q,P)
let P, Q be finite without_zero Subset of NAT ; :: thesis: ( [:P,Q:] c= Indices M & card P = card Q implies Det (EqSegm M,P,Q) = Det (EqSegm (M @ ),Q,P) )
assume that
A1: [:P,Q:] c= Indices M and
A2: card P = card Q ; :: thesis: Det (EqSegm M,P,Q) = Det (EqSegm (M @ ),Q,P)
EqSegm M,P,Q = Segm M,P,Q by A2, Def3
.= (Segm (M @ ),Q,P) @ by A1, A2, Th62
.= (EqSegm (M @ ),Q,P) @ by A2, Def3 ;
hence Det (EqSegm M,P,Q) = Det (EqSegm (M @ ),Q,P) by A2, MATRIXR2:43; :: thesis: verum