let n be Nat; for a being Element of F_Real
for ra being Real
for A being Matrix of n,F_Real
for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
let a be Element of F_Real; for ra being Real
for A being Matrix of n,F_Real
for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
let ra be Real; for A being Matrix of n,F_Real
for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
let A be Matrix of n,F_Real; for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
let rA be Matrix of n,REAL; ( a = ra & A = rA implies a * A = ra * rA )
assume that
A1:
a = ra
and
A2:
A = rA
; a * A = ra * rA
ra * rA =
MXF2MXR (a * (MXR2MXF rA))
by A1, MATRIXR1:def 7
.=
MXF2MXR (a * A)
by A2, MATRIXR1:def 1
;
hence
a * A = ra * rA
by MATRIXR1:def 2; verum