let a, b be Complex; :: thesis: <*a*> (#) <*b*> = <*(a * b)*>
( dom <*a*> = Seg 1 & dom <*b*> = Seg 1 & dom <*(a * b)*> = Seg 1 ) by FINSEQ_1:def 8;
then A2: dom (<*a*> (#) <*b*>) = (Seg 1) /\ (Seg 1) by VALUED_1:def 4
.= Seg 1 ;
then 1 in dom (<*a*> (#) <*b*>) ;
then (<*a*> (#) <*b*>) . 1 = (<*a*> . 1) * (<*b*> . 1) by VALUED_1:def 4;
hence <*a*> (#) <*b*> = <*(a * b)*> by A2, FINSEQ_1:def 8; :: thesis: verum