theorem Th68: :: COMPLSP2:79

for a being Element of COMPLEX
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(a * y))| = (a *') * |(x,y)|