set p = the FinSequence of D;
take the FinSequence of D ; :: thesis: the FinSequence of D is D -valued
thus the FinSequence of D is D -valued ; :: thesis: verum