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