(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) is invertible ; :: thesis: verum