reconsider f = f, g = g as FinSequence of D by NEWTON02:103;
f ^ g is D -valued FinSequence ;
hence f ^ g is D -valued ; :: thesis: verum