theorem :: CLOSURE2:16

for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1)