theorem :: INTEGRA9:23

for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)