let f, g be Function; ( dom f = dom g & f c= g implies f = g )
assume that
A1:
dom f = dom g
and
A2:
f c= g
; f = g
for x, y being object holds
( [x,y] in f iff [x,y] in g )
proof
let x,
y be
object ;
( [x,y] in f iff [x,y] in g )
thus
(
[x,y] in f implies
[x,y] in g )
by A2;
( [x,y] in g implies [x,y] in f )
assume A3:
[x,y] in g
;
[x,y] in f
then
x in dom f
by A1, XTUPLE_0:def 12;
then
[x,(f . x)] in f
by FUNCT_1:1;
hence
[x,y] in f
by A2, A3, FUNCT_1:def 1;
verum
end;
hence
f = g
; verum