let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )
let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )
let M be Matrix of n,K; :: 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 by Def3;
hence ( M ~ is invertible & (M ~) ~ = M ) by A1, Def4; :: thesis: verum