theorem :: MATRIX_6:11

for R being Ring
for n being Nat holds ((1. (R,n)) @) ~ = 1. (R,n)