reconsider aa = a as Element of F_Real by XREAL_0:def 1;
set C = MXF2MXR (aa * (MXR2MXF A));
for ea being Element of F_Real st ea = a holds
MXF2MXR (aa * (MXR2MXF A)) = MXF2MXR (ea * (MXR2MXF A)) ;
hence ex b₁ being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b₁ = MXF2MXR (ea * (MXR2MXF A)) ; :: thesis: verum