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 )
assume n > 0 ; :: thesis: 0. K,n <> 1. K,n
then n >= 0 + 1 by INT_1:20;
then 1 in Seg n ;
then A1: [1,1] in [:(Seg n),(Seg n):] by ZFMISC_1:106;
assume A2: 0. K,n = 1. K,n ; :: thesis: contradiction
A3: ( Indices (0. K,n) = Indices (1. K,n) & Indices (1. K,n) = [:(Seg n),(Seg n):] ) by MATRIX_1:25, MATRIX_1:27;
then (0. K,n) * 1,1 = 0. K by A1, MATRIX_1:30;
then 0. K = 1. K by A1, A2, A3, MATRIX_1:def 12;
hence contradiction ; :: thesis: verum