for a being Real
for G being FinSequence of REAL holds dom G = dom (a * G) by VALUED_1:def 5;