theorem Th1: :: PARTFUN1:1

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