theorem Th1: :: GLIB_010:1

for A, B, C, D being Function st D * A = C | (dom A) holds
(D | (dom B)) * A = C | (dom (B * A))