let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for rA being Matrix of n,REAL st a = ra & A = rA holds
a * A = ra * rA
let rA be Matrix of n,REAL; :: thesis: ( a = ra & A = rA implies a * A = ra * rA )
assume that
A1: a = ra and
A2: A = rA ; :: thesis: 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; :: thesis: verum