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