let n be Nat; :: thesis: for K being Field holds (1. (K,n)) @ = 1. (K,n)
let K be Field; :: thesis: (1. (K,n)) @ = 1. (K,n)
per cases ( n > 0 or n = 0 ) by NAT_1:3;
suppose A1: n > 0 ; :: thesis: (1. (K,n)) @ = 1. (K,n)
A2: len (1. (K,n)) = n by MATRIX_0:24;
A3: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A4: for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
(1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) )
assume A5: [i,j] in Indices (1. (K,n)) ; :: thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j)
then ( i in Seg n & j in Seg n ) by A3, ZFMISC_1:87;
then A6: [j,i] in Indices (1. (K,n)) by A3, ZFMISC_1:87;
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j)
hence (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) by A5, MATRIX_0:def 6; :: thesis: verum
end;
suppose i <> j ; :: thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j)
then ( (1. (K,n)) * (i,j) = 0. K & (1. (K,n)) * (j,i) = 0. K ) by A5, A6, MATRIX_1:def 3;
hence (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) by A6, MATRIX_0:def 6; :: thesis: verum
end;
end;
end;
A7: width (1. (K,n)) = n by MATRIX_0:24;
then ( len ((1. (K,n)) @) = width (1. (K,n)) & width ((1. (K,n)) @) = len (1. (K,n)) ) by A1, MATRIX_0:54;
hence (1. (K,n)) @ = 1. (K,n) by A7, A2, A4, MATRIX_0:21; :: thesis: verum
end;
suppose n = 0 ; :: thesis: (1. (K,n)) @ = 1. (K,n)
hence (1. (K,n)) @ = 1. (K,n) by MATRIX_0:45; :: thesis: verum
end;
end;