theorem Th15: :: ANPROJ_8:17

for A, B being Matrix of F_Real
for RA, RB being Matrix of REAL st A = RA & B = RB holds
A * B = RA * RB