for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence by Lm2;