dom (f <++> g) = (dom f) /\ (dom g) by VALUED_2:def 45;
hence f <++> g is FinSequence-like by VALUED_1:19; :: thesis: verum