let f1, f2 be Function; :: thesis: ( dom f1 = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies f1 . a = y ) & ( H . a <> x implies f1 . a = H . a ) ) ) & dom f2 = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies f2 . a = y ) & ( H . a <> x implies f2 . a = H . a ) ) ) implies f1 = f2 )
assume that
A1: dom f1 = dom H and
A2: for a being object st a in dom H holds
( ( H . a = x implies f1 . a = y ) & ( H . a <> x implies f1 . a = H . a ) ) and
A3: dom f2 = dom H and
A4: for a being object st a in dom H holds
( ( H . a = x implies f2 . a = y ) & ( H . a <> x implies f2 . a = H . a ) ) ; :: thesis: f1 = f2

now :: thesis: for a being object st a in dom H holds
f1 . a = f2 . a

let a be object ; :: thesis: ( a in dom H implies f1 . a = f2 . a )
assume A5: a in dom H ; :: thesis: f1 . a = f2 . a
then A6: ( H . a <> x implies f1 . a = H . a ) by A2;
( H . a = x implies f1 . a = y ) by A2, A5;
hence f1 . a = f2 . a by A4, A5, A6; :: thesis: verum

end;

hence f1 = f2 by A1, A3, FUNCT_1:2; :: thesis: verum