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

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