take N-Str(# {0},f #) ; :: thesis: ( not N-Str(# {0},f #) is empty & N-Str(# {0},f #) is strict )
thus ( not N-Str(# {0},f #) is empty & N-Str(# {0},f #) is strict ) ; :: thesis: verum