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