rng (f * <:p,q:>) c= D by RELAT_1:def 19;
hence f * <:p,q:> is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum