theorem Th16: :: MATRIX_6:16
for n being Nat
for K being Field
for M being Matrix of n,K st M is invertible holds
( M ~ is invertible & (M ~) ~ = M )