<*d,e*> = <*d*> ^ <*e*> by FINSEQ_1:def 9;
hence <*d,e*> is Element of D * by FINSEQ_1:def 11; :: thesis: verum