let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K holds
( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
let K be Field; :: thesis: for A being Matrix of n,K holds
( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
let A be Matrix of n,K; :: thesis: ( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
A1: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
thus ( A = 1. (K,n) implies for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) ) :: thesis: ( ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) ) implies A = 1. (K,n) )

proof

assume A2: A = 1. (K,n) ; :: thesis: for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K))
let i, j be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
assume ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: A * (i,j) = IFEQ (i,j,(1. K),(0. K))
then A3: [i,j] in Indices A by MATRIX_0:31;

per cases ( i = j or i <> j ) ;

suppose A4: i = j ; :: thesis: A * (i,j) = IFEQ (i,j,(1. K),(0. K))

then A * (i,j) = 1. K by A2, A3, MATRIX_1:def 3;
hence A * (i,j) = IFEQ (i,j,(1. K),(0. K)) by A4, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A5: i <> j ; :: thesis: A * (i,j) = IFEQ (i,j,(1. K),(0. K))

then A * (i,j) = 0. K by A2, A3, MATRIX_1:def 3;
hence A * (i,j) = IFEQ (i,j,(1. K),(0. K)) by A5, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

A6: ( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_0:24;
A7: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A8: width A = n by MATRIX_0:24;
thus ( ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) ) implies A = 1. (K,n) ) :: thesis: verum

proof

assume A9: for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) ; :: thesis: A = 1. (K,n)
A10: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (1. (K,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = (1. (K,n)) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume A11: [i,j] in Indices A ; :: thesis: A * (i,j) = (1. (K,n)) * (i,j)
then j in Seg n by A8, ZFMISC_1:87;
then A12: ( 1 <= j & j <= n ) by FINSEQ_1:1;
i in Seg n by A1, A11, ZFMISC_1:87;
then ( 1 <= i & i <= n ) by FINSEQ_1:1;
then A13: A * (i0,j0) = IFEQ (i0,j0,(1. K),(0. K)) by A9, A12;

per cases ( i0 = j0 or i0 <> j0 ) ;

suppose A14: i0 = j0 ; :: thesis: A * (i,j) = (1. (K,n)) * (i,j)

then A * (i0,j0) = 1_ K by A13, FUNCOP_1:def 8;
hence A * (i,j) = (1. (K,n)) * (i,j) by A1, A7, A11, A14, MATRIX_1:def 3; :: thesis: verum

end;

suppose A15: i0 <> j0 ; :: thesis: A * (i,j) = (1. (K,n)) * (i,j)

then A * (i0,j0) = 0. K by A13, FUNCOP_1:def 8;
hence A * (i,j) = (1. (K,n)) * (i,j) by A1, A7, A11, A15, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

( len A = len (1. (K,n)) & width A = width (1. (K,n)) ) by A6, MATRIX_0:24;
hence A = 1. (K,n) by A10, MATRIX_0:21; :: thesis: verum

end;