let A, B be Matrix of F_Real; :: thesis: for RA, RB being Matrix of REAL st A = RA & B = RB holds
A * B = RA * RB
let RA, RB be Matrix of REAL; :: thesis: ( A = RA & B = RB implies A * B = RA * RB )
assume that
A1: A = RA and
A2: B = RB ; :: thesis: A * B = RA * RB
RA * RB = MXF2MXR ((MXR2MXF RA) * (MXR2MXF RB)) by MATRIXR1:def 6
.= MXF2MXR (A * (MXR2MXF RB)) by A1, MATRIXR1:def 1
.= MXF2MXR (A * B) by A2, MATRIXR1:def 1 ;
then MXR2MXF (RA * RB) = A * B by Th14;
hence A * B = RA * RB by MATRIXR1:def 1; :: thesis: verum