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) by Def2;
then 1. (K,n) is invertible by Def3;
hence ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by A1, Def4; :: thesis: verum