let a be Complex; :: thesis: for n being non zero Nat
for f being b₁ -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>
let n be non zero Nat; :: thesis: for f being n -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>
let f be n -element complex-valued FinSequence; :: thesis: <*a*> + f = <*(a + (f . 1))*>
reconsider g = <*a*> as 1 -element complex-valued FinSequence ;
A2: len (g + f) = 1 by CARD_1:def 7;
then 1 in dom (g + f) by FINSEQ_3:25;
then (<*a*> + f) . 1 = (<*a*> . 1) + (f . 1) by VALUED_1:def 1;
hence <*a*> + f = <*(a + (f . 1))*> by A2, FINSEQ_1:40; :: thesis: verum