let a, b be Complex; :: thesis: for n being non trivial Nat
for f being b₁ -element complex-valued FinSequence holds <*a,b*> + f = <*(a + (f . 1)),(b + (f . 2))*>
let n be non trivial Nat; :: thesis: 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; :: thesis: <*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; :: thesis: verum