theorem Th4: :: PARTFUN2:4

for C, D, E being non empty set
for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)