let R be Ring; :: thesis: for n being Nat
for M being Matrix of n,R st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )
let n be Nat; :: thesis: for M being Matrix of n,R st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )
let M be Matrix of n,R; :: thesis: ( M is invertible implies ( M ~ is invertible & (M ~) ~ = M ) )
assume M is invertible ; :: thesis: ( M ~ is invertible & (M ~) ~ = M )
then A1: M ~ is_reverse_of M by Def4;
then M ~ is invertible ;
hence ( M ~ is invertible & (M ~) ~ = M ) by A1, Def4; :: thesis: verum