reconsider g = g as XFinSequence of D by Def8;
f ^ g is XFinSequence of D ;
hence f ^ g is Element of D ^omega by Def8; :: thesis: verum