let C1, C2 be Matrix of REAL ; :: thesis: ( ( for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ) implies C1 = C2 )
assume A1: ( ( for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ) ) ; :: thesis: C1 = C2
reconsider aa = a as Element of F_Real by XREAL_0:def 1;
C2 = MXF2MXR (aa * (MXR2MXF A)) by A1;
hence C1 = C2 by A1; :: thesis: verum