theorem :: MATRIXR2:83

for n being Nat
for A, B being Matrix of n,REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )