let K be Field; :: thesis: for n being Element of NAT
for A being Matrix of n,K
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds
(SwapDiagonal K,n,1) * i,j = 0. K
let n be Element of NAT ; :: thesis: for A being Matrix of n,K
for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds
(SwapDiagonal K,n,1) * i,j = 0. K
let A be Matrix of n,K; :: thesis: for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds
(SwapDiagonal K,n,1) * i,j = 0. K
set A = SwapDiagonal K,n,1;
let i, j be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n & i <> j implies (SwapDiagonal K,n,1) * i,j = 0. K )
assume ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: ( not i <> j or (SwapDiagonal K,n,1) * i,j = 0. K )
then A1: [i,j] in Indices (SwapDiagonal K,n,1) by MATRIX_1:38;
SwapDiagonal K,n,1 = 1. K,n by FINSEQ_7:21;
hence ( not i <> j or (SwapDiagonal K,n,1) * i,j = 0. K ) by A1, MATRIX_1:def 12; :: thesis: verum