let n be Nat; :: thesis: for K being Field
for a being Element of K holds (n,n --> a) @ = n,n --> a
let K be Field; :: thesis: for a being Element of K holds (n,n --> a) @ = n,n --> a
let a be Element of K; :: thesis: (n,n --> a) @ = n,n --> a

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

suppose A1: n > 0 ; :: thesis: (n,n --> a) @ = n,n --> a

A2: ( width (n,n --> a) = n & len (n,n --> a) = n & Indices (n,n --> a) = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
then A3: ( width ((n,n --> a) @ ) = width (n,n --> a) & len ((n,n --> a) @ ) = len (n,n --> a) ) by A1, MATRIX_2:12;
for i, j being Nat st [i,j] in Indices ((n,n --> a) @ ) holds
((n,n --> a) @ ) * i,j = (n,n --> a) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((n,n --> a) @ ) implies ((n,n --> a) @ ) * i,j = (n,n --> a) * i,j )
assume [i,j] in Indices ((n,n --> a) @ ) ; :: thesis: ((n,n --> a) @ ) * i,j = (n,n --> a) * i,j
then A4: [i,j] in Indices (n,n --> a) by MATRIX_1:27;
then ( i in Seg n & j in Seg n ) by A2, ZFMISC_1:106;
then [j,i] in Indices (n,n --> a) by A2, ZFMISC_1:106;
then ( ((n,n --> a) @ ) * i,j = (n,n --> a) * j,i & (n,n --> a) * j,i = a ) by MATRIX_1:def 7, MATRIX_2:1;
hence ((n,n --> a) @ ) * i,j = (n,n --> a) * i,j by A4, MATRIX_2:1; :: thesis: verum

end;

hence (n,n --> a) @ = n,n --> a by A3, MATRIX_1:21; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (n,n --> a) @ = n,n --> a

then ( len ((n,n --> a) @ ) = 0 & len (n,n --> a) = 0 ) by MATRIX_1:def 3;
hence (n,n --> a) @ = n,n --> a by CARD_2:83; :: thesis: verum

end;

end;