theorem Th64: :: MATRIX13:64

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds
( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )