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

proof

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

now

let c be Element of C; :: thesis: ( ( c in dom g implies ( c in dom f & f /. c in X ) ) & ( c in dom f & f /. c in X implies c in dom g ) )
thus ( c in dom g implies ( c in dom f & f /. c in X ) ) :: thesis: ( c in dom f & f /. c in X implies c in dom g )

proof

assume c in dom g ; :: thesis: ( c in dom f & f /. c in X )
then ( c in dom f & f . c in X ) by A1, FUNCT_1:86;
hence ( c in dom f & f /. c in X ) by PARTFUN1:def 8; :: thesis: verum

end;

assume ( c in dom f & f /. c in X ) ; :: thesis: c in dom g
then ( c in dom f & f . c in X ) by PARTFUN1:def 8;
hence c in dom g by A1, FUNCT_1:86; :: thesis: verum

end;

hence for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ; :: 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 A2: c in dom g ; :: thesis: g /. c = f /. c
then g . c = f . c by A1, FUNCT_1:87;
then A3: g /. c = f . c by A2, PARTFUN1:def 8;
c in dom f by A1, A2, FUNCT_1:86;
hence g /. c = f /. c by A3, PARTFUN1:def 8; :: thesis: verum

end;

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

A5: now

let x be set ; :: thesis: ( ( x in dom g implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in dom g ) )
thus ( x in dom g implies ( x in dom f & f . x in X ) ) :: thesis: ( x in dom f & f . x in X implies x in dom g )

proof

assume A6: x in dom g ; :: thesis: ( x in dom f & f . x in X )
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A4, A6;
hence ( x in dom f & f . x in X ) by PARTFUN1:def 8; :: thesis: verum

end;

assume A7: ( x in dom f & f . x in X ) ; :: thesis: x in dom g
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A7, PARTFUN1:def 8;
hence x in dom g by A4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom g implies g . x = f . x )
assume A8: x in dom g ; :: thesis: g . x = f . x
then reconsider x1 = x as Element of C ;
A9: x1 in dom f by A4, A8;
g /. x1 = f /. x1 by A4, A8;
then g . x1 = f /. x1 by A8, PARTFUN1:def 8;
hence g . x = f . x by A9, PARTFUN1:def 8; :: thesis: verum

end;

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