dom <:f1,f2:> = (dom f1) /\ (dom f2) by FUNCT_3:def 7;
hence <:f1,f2:> is FinSequence-like by VALUED_1:19; :: thesis: verum