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)|
|(x,(a * y))| = |((a * y),x)| *' by Th64
.= (a * |(y,x)|) *' by A1, Th67
.= (a *') * (|(y,x)| *') by COMPLEX1:35
.= (a *') * |(x,y)| by Th64 ;
hence |(x,(a * y))| = (a *') * |(x,y)| ; :: thesis: verum