let n be Nat; :: thesis: for K being Field st n > 0 holds
0. (K,n) <> 1. (K,n)
let K be Field; :: thesis: ( n > 0 implies 0. (K,n) <> 1. (K,n) )
A1: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume n > 0 ; :: thesis: 0. (K,n) <> 1. (K,n)
then n >= 0 + 1 by INT_1:7;
then 1 in Seg n ;
then A2: [1,1] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
assume A3: 0. (K,n) = 1. (K,n) ; :: thesis: contradiction
Indices (0. (K,n)) = Indices (1. (K,n)) by MATRIX_0:26;
then (0. (K,n)) * (1,1) = 0. K by A2, A1, MATRIX_1:1;
then 0. K = 1. K by A2, A3, A1, MATRIX_1:def 3;
hence contradiction ; :: thesis: verum