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