theorem Th4: :: INTEGRA5:4
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C