let a be Element of COMPLEX ; :: thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(a * y))| = (a *' ) * |(x,y)|
let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |(x,(a * y))| = (a *' ) * |(x,y)| )
assume A1: len x = len y ; :: thesis: |(x,(a * y))| = (a *' ) * |(x,y)|
len (a * y) = len y by Th3;
then |(x,(a * y))| = |((a * y),x)| *' by A1, Th75
.= (a * |(y,x)|) *' by A1, Th78
.= (a *' ) * (|(y,x)| *' ) by COMPLEX1:121
.= (a *' ) * |(x,y)| by A1, Th75 ;
hence |(x,(a * y))| = (a *' ) * |(x,y)| ; :: thesis: verum