take the empty FinSequence of D * ; :: thesis: the empty FinSequence of D * is double-one-to-one
thus the empty FinSequence of D * is double-one-to-one ; :: thesis: verum