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