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