for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X by Lm2;