let n be Nat; :: thesis: for K being Field holds

( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible )

let K be Field; :: thesis: ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible )

(1. (K,n)) * (1. (K,n)) = 1. (K,n) by MATRIX_3:18;

then A1: 1. (K,n) is_reverse_of 1. (K,n) ;

then 1. (K,n) is invertible ;

hence ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by A1, Def4; :: thesis: verum

( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible )

let K be Field; :: thesis: ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible )

(1. (K,n)) * (1. (K,n)) = 1. (K,n) by MATRIX_3:18;

then A1: 1. (K,n) is_reverse_of 1. (K,n) ;

then 1. (K,n) is invertible ;

hence ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by A1, Def4; :: thesis: verum