let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K holds
( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
let K be Field; :: thesis: for A being Matrix of n,K holds
( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
let A be Matrix of n,K; :: thesis: ( A = 0. K,n iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K )
A2: ( len A = n & width A = n & Indices A = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
thus ( A = 0. K,n implies for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K ) :: thesis: ( ( for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K ) implies A = 0. K,n )

proof

assume A = 0. K,n ; :: thesis: for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K
then B1b: A = 0. K,n,n by MATRIX_3:def 1;
thus for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K :: thesis: verum

proof

let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies A * i,j = 0. K )
assume C1: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: A * i,j = 0. K
[i,j] in Indices A by C1, MATRIX_1:38;
hence A * i,j = 0. K by B1b, MATRIX_3:3; :: thesis: verum

end;

end;

assume B0: for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * i,j = 0. K ; :: thesis: A = 0. K,n
for i, j being Nat st [i,j] in Indices A holds
A * i,j = (A + A) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * i,j = (A + A) * i,j )
assume B1: [i,j] in Indices A ; :: thesis: A * i,j = (A + A) * i,j
then ( i in Seg n & j in Seg n ) by A2, ZFMISC_1:106;
then B3: ( 1 <= i & i <= n & 1 <= j & j <= n ) by FINSEQ_1:3;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;
B4: A * i0,j0 = 0. K by B3, B0;
(A + A) * i,j = (0. K) + (A * i,j) by B4, B1, MATRIX_3:def 3
.= A * i,j by RLVECT_1:10 ;
hence A * i,j = (A + A) * i,j ; :: thesis: verum

end;

then A = A + A by MATRIX_1:28;
then A = 0. K,n,n by A2, MATRIX_4:6;
hence A = 0. K,n by MATRIX_3:def 1; :: thesis: verum