let a be Complex; :: thesis: for f being complex-valued FinSequence holds ((len f) |-> a) (#) f = a (#) f
let f be complex-valued FinSequence; :: thesis: ((len f) |-> a) (#) f = a (#) f
len ((len f) |-> a) = len f ;
then dom ((len f) |-> a) = dom f by FINSEQ_3:29;
then A1: (dom ((len f) |-> a)) /\ (dom f) = dom (a (#) f) by VALUED_1:def 5;
then A2: dom (((len f) |-> a) (#) f) = dom (a (#) f) by VALUED_1:def 4;
for x being object st x in dom (((len f) |-> a) (#) f) holds
(((len f) |-> a) (#) f) . x = (a (#) f) . x

proof

let x be object ; :: thesis: ( x in dom (((len f) |-> a) (#) f) implies (((len f) |-> a) (#) f) . x = (a (#) f) . x )
assume B1: x in dom (((len f) |-> a) (#) f) ; :: thesis: (((len f) |-> a) (#) f) . x = (a (#) f) . x
reconsider x = x as non zero Nat by B1, FINSEQ_3:25;
( len ((len f) |-> a) >= x & x >= 1 ) by A1, A2, B1, FINSEQ_3:25;
then ex k being Nat st len f = x + k by NAT_1:10;
then reconsider k = (len f) - x as Nat ;
(((len f) |-> a) (#) f) . x = (((x + k) |-> a) . x) * (f . x) by B1, VALUED_1:def 4
.= (a (#) f) . x by A2, B1, VALUED_1:def 5 ;
hence (((len f) |-> a) (#) f) . x = (a (#) f) . x ; :: thesis: verum

end;

hence ((len f) |-> a) (#) f = a (#) f by A2, FUNCT_1:2; :: thesis: verum