let X be set ; :: thesis:
let C, D be non empty set ; :: thesis:
let f, g be PartFunc of C,D; :: thesis:
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:

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

end;

end;

end;

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

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

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

end;

assume that
A10: x in dom f and
A11: f . x in X ; :: thesis:
reconsider x1 = x as Element of C by A10;
f /. x1 in X by A10, A11, PARTFUN1:def 6;
hence x in dom g by A6, A10; :: thesis:

end;

end;