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