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 ;

hence ( M ~ is invertible & (M ~) ~ = M ) by A1, Def4; :: thesis: verum

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 ;

hence ( M ~ is invertible & (M ~) ~ = M ) by A1, Def4; :: thesis: verum