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