theorem Th72: :: MATRIX13:72

for K being Field
for a being Element of K
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 ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))