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_0:31;
SwapDiagonal (K,n,1) = 1. (K,n) by FINSEQ_7:19;
hence ( not i <> j or (SwapDiagonal (K,n,1)) * (i,j) = 0. K ) by A1, MATRIX_1:def 3; :: thesis: verum