theorem Th28: :: GAUSSINT:28

for z being G_RAT
for i being Element of RAT holds RSc_Mult . (i,z) = i * z