let f, g be Function; ( f c= g iff ( dom f c= dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) )
thus
( f c= g implies ( dom f c= dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) )
( dom f c= dom g & ( for x being object st x in dom f holds
f . x = g . x ) implies f c= g )
assume that
A2:
dom f c= dom g
and
A3:
for x being object st x in dom f holds
f . x = g . x
; f c= g
let x, y be object ; RELAT_1:def 3 ( not [x,y] in f or [x,y] in g )
assume A4:
[x,y] in f
; [x,y] in g
then A5:
x in dom f
by FUNCT_1:1;
y = f . x
by A4, FUNCT_1:1;
then
y = g . x
by A3, A5;
hence
[x,y] in g
by A2, A5, FUNCT_1:def 2; verum