let a, b be Complex; :: thesis: a (#) <*b*> = <*(a * b)*>
A1: ( dom <*(a * b)*> = Seg 1 & dom <*b*> = Seg 1 ) by FINSEQ_1:def 8;
for x being object st x in Seg 1 holds
<*(a * b)*> . x = a * (<*b*> . x)

proof

let x be object ; :: thesis: ( x in Seg 1 implies <*(a * b)*> . x = a * (<*b*> . x) )
assume x in Seg 1 ; :: thesis: <*(a * b)*> . x = a * (<*b*> . x)
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*(a * b)*> . x = a * (<*b*> . x) ; :: thesis: verum

end;

hence a (#) <*b*> = <*(a * b)*> by A1, VALUED_1:def 5; :: thesis: verum