dom (f to_power g) = (dom f) /\ (dom g) by Def6;
hence f to_power g is FinSequence-like by VALUED_1:19; :: thesis: verum