let f, g be Function; :: thesis: ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) implies f = g )
assume that
A1: dom f = dom g and
A2: for x being object st x in dom f holds
f . x = g . x ; :: thesis: f = g
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in f or [x,y] in g ) & ( not [x,y] in g or [x,y] in f ) )
thus ( [x,y] in f implies [x,y] in g ) :: thesis: ( not [x,y] in g or [x,y] in f )

proof

assume A3: [x,y] in f ; :: thesis: [x,y] in g
then A4: x in dom f by XTUPLE_0:def 12;
reconsider y = y as set by TARSKI:1;
f . x = y by A3, Def2, A4;
then g . x = y by A2, A4;
hence [x,y] in g by A1, A4, Def2; :: thesis: verum

end;

assume A5: [x,y] in g ; :: thesis: [x,y] in f
then A6: x in dom g by XTUPLE_0:def 12;
reconsider y = y as set by TARSKI:1;
g . x = y by A5, Def2, A6;
then f . x = y by A1, A2, A6;
hence [x,y] in f by A1, A6, Def2; :: thesis: verum