theorem Th44: :: MATRIX14:44

for K being Field
for n being Element of NAT
for A being Matrix of n,K
for i being Nat st 1 <= i & i <= n holds
(SwapDiagonal (K,n,1)) * (i,i) = 1. K