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

|(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