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)

let K be Field; :: thesis: (1. (K,n)) @ = 1. (K,n)

per cases
( n > 0 or n = 0 )
by NAT_1:3;

end;

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)

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;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

A7:
width (1. (K,n)) = n
by MATRIX_0:24;
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;

end;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;

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