let f, g be Function; :: thesis: ( dom f = dom g & f c= g implies f = g )
assume that
A1: dom f = dom g and
A2: f c= g ; :: thesis: f = g
for x, y being object holds
( [x,y] in f iff [x,y] in g )
proof
let x, y be object ; :: thesis: ( [x,y] in f iff [x,y] in g )
thus ( [x,y] in f implies [x,y] in g ) by A2; :: thesis: ( [x,y] in g implies [x,y] in f )
assume A3: [x,y] in g ; :: thesis: [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; :: thesis: verum
end;
hence f = g ; :: thesis: verum