let K be Field; 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; 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; ( [: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
; 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; verum