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

set A2 = 0. (K,n);
set B2 = 0. (K,n);
set A3 = 0. (K,n,n);
assume A1: 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
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies A * (i,j) = 0. K )
assume ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: A * (i,j) = 0. K
then [i,j] in Indices (0. (K,n)) by MATRIX_0:31;
then ( 0. (K,n,n) = 0. (K,n) & ((0. (K,n)) + (0. (K,n))) * (i,j) = ((0. (K,n)) * (i,j)) + ((0. (K,n)) * (i,j)) ) by MATRIX_3:def 1, MATRIX_3:def 3;
then (0. (K,n)) * (i,j) = ((0. (K,n)) * (i,j)) + ((0. (K,n)) * (i,j)) by MATRIX_3:4;
then ((0. (K,n)) * (i,j)) - ((0. (K,n)) * (i,j)) = ((0. (K,n)) * (i,j)) + (((0. (K,n)) * (i,j)) - ((0. (K,n)) * (i,j))) by RLVECT_1:28
.= ((0. (K,n)) * (i,j)) + (0. K) by RLVECT_1:15
.= (0. (K,n)) * (i,j) by RLVECT_1:4 ;
hence A * (i,j) = 0. K by A1, RLVECT_1:15; :: thesis: verum

end;

A2: len A = n by MATRIX_0:24;
A3: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
A4: width A = n by MATRIX_0:24;
assume A5: 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 * (i,j)) + (A * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = (A * (i,j)) + (A * (i,j)) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume A6: [i,j] in Indices A ; :: thesis: A * (i,j) = (A * (i,j)) + (A * (i,j))
then j in Seg n by A4, ZFMISC_1:87;
then A7: ( 1 <= j & j <= n ) by FINSEQ_1:1;
i in Seg n by A3, A6, ZFMISC_1:87;
then ( 1 <= i & i <= n ) by FINSEQ_1:1;
then A * (i0,j0) = 0. K by A5, A7;
hence A * (i,j) = (A * (i,j)) + (A * (i,j)) by RLVECT_1:4; :: thesis: verum

end;

then A = A + A by A2, MATRIX_3:def 3;
then A = 0. (K,(len A),(width A)) by MATRIX_4:6;
hence A = 0. (K,n) by A2, A4, MATRIX_3:def 1; :: thesis: verum