theorem Th52: :: BKMODEL1:60

for n being Nat
for N being Matrix of n,REAL st N is invertible holds
( N @ is invertible & Inv (N @) = (Inv N) @ )