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:20;
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