take InvShift 1 ; :: thesis: ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero )
thus ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero ) ; :: thesis: verum