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:21, MATRIX_1:38;
hence (SwapDiagonal K,n,1) * i,i = 1. K by MATRIX_1:def 12; :: thesis: verum