theorem Th9: :: MATRIX_6:8

for n being Nat
for R being Ring holds
( (1. (R,n)) ~ = 1. (R,n) & 1. (R,n) is invertible )