theorem Th48: :: MATRIX14:48

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