take the empty FinSequence ; :: thesis: ( the empty FinSequence is empty & the empty FinSequence is Graph-yielding )
thus ( the empty FinSequence is empty & the empty FinSequence is Graph-yielding ) ; :: thesis: verum