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