let h1, h2 be Function; :: thesis: ( dom h1 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) ) & dom h2 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ) implies h1 = h2 )
assume that
A1: dom h1 = (dom f) \/ (dom g) and
A2: for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) and
A3: dom h2 = (dom f) \/ (dom g) and
A4: for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ; :: thesis: h1 = h2
for x being object st x in (dom f) \/ (dom g) holds
h1 . x = h2 . x

proof

let x be object ; :: thesis: ( x in (dom f) \/ (dom g) implies h1 . x = h2 . x )
assume A5: x in (dom f) \/ (dom g) ; :: thesis: h1 . x = h2 . x
then A6: ( not x in dom g implies ( h1 . x = f . x & h2 . x = f . x ) ) by A2, A4;
( x in dom g implies ( h1 . x = g . x & h2 . x = g . x ) ) by A2, A4, A5;
hence h1 . x = h2 . x by A6; :: thesis: verum

end;

hence h1 = h2 by A1, A3; :: thesis: verum