theorem :: COMPLSP2:80

for a, b being Element of COMPLEX
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)