( f is empty or not f is empty ) ;
hence Product f is positive ; :: thesis: verum