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 1
.= Seg 1 ;
then 1 in dom (<*a*> + <*b*>) ;
then (<*a*> + <*b*>) . 1 = (<*a*> . 1) + (<*b*> . 1) by VALUED_1:def 1;
hence <*a*> + <*b*> = <*(a + b)*> by A2, FINSEQ_1:def 8; :: thesis: verum