let n be Nat; :: thesis: for R being Ring holds
( (1. (R,n)) ~ = 1. (R,n) & 1. (R,n) is invertible )
let R be Ring; :: thesis: ( (1. (R,n)) ~ = 1. (R,n) & 1. (R,n) is invertible )
(1. (R,n)) * (1. (R,n)) = 1. (R,n) by MATRIX_3:18;
then 1. (R,n) is_reverse_of 1. (R,n) ;
hence ( (1. (R,n)) ~ = 1. (R,n) & 1. (R,n) is invertible ) by Def4; :: thesis: verum