for i, j being Nat st [i,j] in Indices ((n,n) --> 1) holds
((n,n) --> 1) * (i,j) >= 0 by MATRIX_2:1;
hence for b₁ being Matrix of n, REAL st b₁ = (n,n) --> 1 holds
b₁ is Nonnegative by Def4; :: thesis: verum