let a, b be Element of COMPLEX ; :: thesis: 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)|)
let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|) )
assume A1: ( len x = len y & len y = len z ) ; :: thesis: |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)
A2: len (a * x) = len x by Th3;
len (b * y) = len y by Th3;
then |(((a * x) + (b * y)),z)| = |((a * x),z)| + |((b * y),z)| by A1, A2, Th66
.= (a * |(x,z)|) + |((b * y),z)| by A1, Th78
.= (a * |(x,z)|) + (b * |(y,z)|) by A1, Th78 ;
hence |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|) ; :: thesis: verum