theorem :: FINSEQ_1:62

for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *