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