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