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 4;
hence <*a,b*> (#) f = <*(a * (f . 1)),(b * (f . 2))*> by A1, FINSEQ_1:44; :: thesis: verum