let x, y be FinSequence of COMPLEX ; :: thesis: for a being Element of COMPLEX st len x = len y holds
mlt ((a * x),y) = a * (mlt (x,y))
let a be Element of COMPLEX ; :: thesis: ( len x = len y implies mlt ((a * x),y) = a * (mlt (x,y)) )
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
assume len x = len y ; :: thesis: mlt ((a * x),y) = a * (mlt (x,y))
then mlt ((a * x),y) = a * (mlt (x9,y9)) by Th15
.= a * (mlt (x,y)) ;
hence mlt ((a * x),y) = a * (mlt (x,y)) ; :: thesis: verum