take T = the empty Function; :: thesis: ( T is complex-functions-valued & T is FinSequence-yielding )
thus ( T is complex-functions-valued & T is FinSequence-yielding ) ; :: thesis: verum