let n be Nat; :: thesis: for R being commutative Ring
for M being Matrix of n,R st M is invertible holds
( M @ is invertible & (M @) ~ = (M ~) @ )
let R be commutative Ring; :: 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 A1: M is invertible ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )
set M1 = M @ ;
set M2 = (M ~) @ ;

per cases ( n > 0 or n = 0 ) by NAT_1:3;

suppose A2: n > 0 ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )

A3: ( width M = n & width (M ~) = n ) by MATRIX_0:24;
len M = n by MATRIX_0:24;
then A4: ((M ~) * M) @ = (M @) * ((M ~) @) by A2, A3, MATRIX_3:22;
A5: M ~ is_reverse_of M by A1, Def4;
then A6: (M @) * ((M ~) @) = 1. (R,n) by A4, Th11;
len (M ~) = n by MATRIX_0:24;
then (M * (M ~)) @ = ((M ~) @) * (M @) by A2, A3, MATRIX_3:22;
then (M @) * ((M ~) @) = ((M ~) @) * (M @) by A5, A4;
then A7: M @ is_reverse_of (M ~) @ by A6;
then M @ is invertible ;
hence ( M @ is invertible & (M @) ~ = (M ~) @ ) by A7, Def4; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )

then A8: M = 1. (R,n) by MATRIX_0:45;
then A9: M @ = 1. (R,n) by Th11;
then (M @) ~ = 1. (R,n) by Th9;
hence ( M @ is invertible & (M @) ~ = (M ~) @ ) by A8, A9; :: thesis: verum

end;

end;