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 that
A1: len x = len y and
A2: len y = len z ; :: thesis: |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)
( len (a * x) = len x & len (b * y) = len y ) by Th3;
then |(((a * x) + (b * y)),z)| = |((a * x),z)| + |((b * y),z)| by A1, A2, Th55
.= (a * |(x,z)|) + |((b * y),z)| by A1, A2, Th67
.= (a * |(x,z)|) + (b * |(y,z)|) by A2, Th67 ;
hence |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|) ; :: thesis: verum