let i be Nat; :: thesis: for f being complex-valued FinSequence holds ((id (dom f)) (#) f) . i = i * (f . i)
let f be complex-valued FinSequence; :: thesis: ((id (dom f)) (#) f) . i = i * (f . i)

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: ((id (dom f)) (#) f) . i = i * (f . i)

then (id (dom f)) . i = i by FUNCT_1:17;
hence ((id (dom f)) (#) f) . i = i * (f . i) by VALUED_1:5; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: ((id (dom f)) (#) f) . i = i * (f . i)

then A1: f . i = 0 by FUNCT_1:def 2;
((id (dom f)) (#) f) . i = ((id (dom f)) . i) * (f . i) by VALUED_1:5;
hence ((id (dom f)) (#) f) . i = i * (f . i) by A1; :: thesis: verum

end;

end;