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