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:110;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
assume len x = len y ; :: thesis: mlt (a * x),y = a * (mlt x,y)
then mlt (a * x),y = a * (mlt x9,y9) by Th16
.= a * (mlt x,y) ;
hence mlt (a * x),y = a * (mlt x,y) ; :: thesis: verum