let X be set ; :: thesis: for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let D, C be non empty set ; :: thesis: for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let g, f be PartFunc of C,D; :: thesis: ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
thus ( g = f | X implies ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) ) :: thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) implies g = f | X )

proof

assume A1: g = f | X ; :: thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) )
then A2: ( dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) ) by FUNCT_1:70, RELAT_1:90;
thus dom g = (dom f) /\ X by A1, RELAT_1:90; :: thesis: for c being Element of C st c in dom g holds
g /. c = f /. c
let c be Element of C; :: thesis: ( c in dom g implies g /. c = f /. c )
assume A3: c in dom g ; :: thesis: g /. c = f /. c
then A4: c in dom f by A2, XBOOLE_0:def 4;
g . c = f . c by A1, A3, FUNCT_1:70;
then g /. c = f . c by A3, PARTFUN1:def 8;
hence g /. c = f /. c by A4, PARTFUN1:def 8; :: thesis: verum

end;

assume A5: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) ; :: thesis: g = f | X

now

let x be set ; :: thesis: ( x in dom g implies g . x = f . x )
assume A6: x in dom g ; :: thesis: g . x = f . x
then A7: x in dom f by A5, XBOOLE_0:def 4;
reconsider y = x as Element of C by A6;
g /. y = f /. y by A5, A6;
then g . y = f /. y by A6, PARTFUN1:def 8;
hence g . x = f . x by A7, PARTFUN1:def 8; :: thesis: verum

end;

hence g = f | X by A5, FUNCT_1:68; :: thesis: verum