let f, g be Function; :: thesis: ( dom f = dom g & ( for x being set 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 set st x in dom f holds
f . x = g . x ; :: thesis: f = g
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in f or [x,b₁] in g ) & ( not [x,b₁] in g or [x,b₁] in f ) )
let y be set ; :: 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 RELAT_1:def 4;
then f . x = y by A3, Def4;
then g . x = y by A2, A4;
hence [x,y] in g by A1, A4, Def4; :: thesis: verum

end;

assume A5: [x,y] in g ; :: thesis: [x,y] in f
then A6: x in dom g by RELAT_1:def 4;
then g . x = y by A5, Def4;
then f . x = y by A1, A2, A6;
hence [x,y] in f by A1, A6, Def4; :: thesis: verum