for X, Y, D being set
for F being Functional_Sequence of X,Y st F is with_the_same_dom holds
F || D is with_the_same_dom