let K be Field; :: thesis: 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
let n be Element of NAT ; :: thesis: 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
let A be Matrix of n,K; :: thesis: for i being Nat st 1 <= i & i <= n holds
(SwapDiagonal (K,n,1)) * (i,i) = 1. K
set A = SwapDiagonal (K,n,1);
let i be Nat; :: thesis: ( 1 <= i & i <= n implies (SwapDiagonal (K,n,1)) * (i,i) = 1. K )
assume ( 1 <= i & i <= n ) ; :: thesis: (SwapDiagonal (K,n,1)) * (i,i) = 1. K
then ( SwapDiagonal (K,n,1) = 1. (K,n) & [i,i] in Indices (SwapDiagonal (K,n,1)) ) by FINSEQ_7:19, MATRIX_0:31;
hence (SwapDiagonal (K,n,1)) * (i,i) = 1. K by MATRIX_1:def 3; :: thesis: verum