theorem Th09: :: ANPROJ_9:8

for a, b, c being non zero Element of F_Real
for M1, M2 being Matrix of 3,F_Real st M1 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> & M2 = <*<*(1 / a),0,0*>,<*0,(1 / b),0*>,<*0,0,(1 / c)*>*> holds
( M1 * M2 = 1. (F_Real,3) & M2 * M1 = 1. (F_Real,3) )