theorem Th36:
for
n being
Nat for
K being
Field for
M being
Matrix of
K for
nt,
nt1,
nt9,
nt19 being
Element of
n -tuples_on NAT st
rng nt = rng nt9 &
rng nt1 = rng nt19 & not
Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))