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:8
.= <*(- b)*> . 1 ;
then A2: q = p by A1, FINSEQ_1:40;
<*a*> + <*(- b)*> = <*(a + (- b))*> by APB;
hence <*a*> - <*b*> = <*(a - b)*> by A2, VALUED_1:def 9; :: thesis: verum