reconsider f = f, g = g as XFinSequence of D by AFINSQ_1:def 8;
f ^ g is XFinSequence of D ;
hence f ^ g is Element of D ^omega by AFINSQ_1:def 8; :: thesis: verum