let a, b be Complex; :: thesis: <*a*> /" <*b*> = <*(a * (b "))*>
reconsider p = <*(b ")*> as 1 -element FinSequence ;
reconsider q = <*b*> " as 1 -element FinSequence ;
A1: ( len p = 1 & len q = 1 ) by CARD_1:def 7;
(<*b*> ") . 1 = (<*b*> . 1) " by VALUED_1:10
.= <*(b ")*> . 1 ;
then A2: q = p by A1, FINSEQ_1:40;
<*a*> (#) <*(b ")*> = <*(a * (b "))*> by AMB;
hence <*a*> /" <*b*> = <*(a * (b "))*> by A2, VALUED_1:def 10; :: thesis: verum