theorem Th5: :: GAUSSINT:5

for z being G_INTEG
for i being Integer holds Sc_Mult . (i,z) = i * z