let x, y be FinSequence of COMPLEX ; 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 ; ( 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
; 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))
; verum