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