:: deftheorem defines * MATRIXR1:def 6 :
for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B));