theorem Th51: :: MATRIX14:51

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