let f, g, h be Function; :: thesis: ( f \/ g = h implies for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x )
assume A1: f \/ g = h ; :: thesis: for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x
let x be set ; :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( h . x = f . x & h . x = g . x ) by A1, GRFUNC_1:35;
hence f . x = g . x ; :: thesis: verum