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