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 Element of 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 Element of 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 Element of 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_1:25;
thus ( A = 1. K,n implies for i, j being Element of 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 Element of 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 Element of 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 Element of 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_1:38;

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 12;
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 12;
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_1:25;
A7: Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A8: width A = n by MATRIX_1:25;
thus ( ( for i, j being Element of 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 Element of 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 13;
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:106;
then A12: ( 1 <= j & j <= n ) by FINSEQ_1:3;
i in Seg n by A1, A11, ZFMISC_1:106;
then ( 1 <= i & i <= n ) by FINSEQ_1:3;
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 12; :: 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 12; :: thesis: verum

end;

end;

end;

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

end;