let X be set ; for f, g being Function st dom g = (dom f) /\ X & ( for x being object st x in dom g holds
g . x = f . x ) holds
g = f | X
let f, g be Function; ( dom g = (dom f) /\ X & ( for x being object st x in dom g holds
g . x = f . x ) implies g = f | X )
assume that
A1:
dom g = (dom f) /\ X
and
A2:
for x being object st x in dom g holds
g . x = f . x
; g = f | X
now for x, y being object holds
( ( [x,y] in g implies ( x in X & [x,y] in f ) ) & ( x in X & [x,y] in f implies [x,y] in g ) )let x,
y be
object ;
( ( [x,y] in g implies ( x in X & [x,y] in f ) ) & ( x in X & [x,y] in f implies [x,y] in g ) )hereby ( x in X & [x,y] in f implies [x,y] in g )
assume A3:
[x,y] in g
;
( x in X & [x,y] in f )then A4:
x in dom g
by XTUPLE_0:def 12;
hence
x in X
by A1, XBOOLE_0:def 4;
[x,y] in fA5:
x in dom f
by A1, A4, XBOOLE_0:def 4;
reconsider yy =
y as
set by TARSKI:1;
yy =
g . x
by A3, A4, Def2
.=
f . x
by A2, A4
;
hence
[x,y] in f
by A5, Def2;
verum
end; assume A6:
x in X
;
( [x,y] in f implies [x,y] in g )assume A7:
[x,y] in f
;
[x,y] in gthen A8:
x in dom f
by XTUPLE_0:def 12;
then A9:
x in dom g
by A1, A6, XBOOLE_0:def 4;
reconsider yy =
y as
set by TARSKI:1;
yy =
f . x
by A7, A8, Def2
.=
g . x
by A2, A9
;
hence
[x,y] in g
by A9, Def2;
verum end;
hence
g = f | X
by RELAT_1:def 11; verum