for n being Element of NAT
for K being Field
for A being Matrix of n,K st A is invertible holds
( A @ is invertible & (A @) ~ = (A ~) @ )