theorem Th2: :: PARTFUN1:2

for f, g, h being Function st f \/ g = h holds
for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x