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