theorem Th30: :: MESFUN7C:30

for X being non empty set
for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)