theorem Th46: :: BKMODEL1:54

for n being 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