let n be Nat; :: thesis: for K being Field holds 1. (K,n) is Self_Reversible
let K be Field; :: thesis: 1. (K,n) is Self_Reversible
( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by MATRIX_6:8;
hence 1. (K,n) is Self_Reversible by Def4; :: thesis: verum