F = <*> (D *) ;
then FlattenSeq F = <*> D by Th2;
hence FlattenSeq F is empty ; :: thesis: verum