let X be set ; :: thesis: for h being one-to-one Function holds (h | X) " = (h " ) | (h .: X)
let h be one-to-one Function; :: thesis: (h | X) " = (h " ) | (h .: X)
reconsider hX = h | X as one-to-one Function ;

now

let r be set ; :: thesis: ( ( r in dom ((h | X) " ) implies r in dom ((h " ) | (h .: X)) ) & ( r in dom ((h " ) | (h .: X)) implies r in dom ((h | X) " ) ) )
thus ( r in dom ((h | X) " ) implies r in dom ((h " ) | (h .: X)) ) :: thesis: ( r in dom ((h " ) | (h .: X)) implies r in dom ((h | X) " ) )

proof

assume r in dom ((h | X) " ) ; :: thesis: r in dom ((h " ) | (h .: X))
then r in rng hX by FUNCT_1:55;
then consider g being set such that
A1: g in dom (h | X) and
A2: (h | X) . g = r by FUNCT_1:def 5;
A3: h . g = r by A1, A2, FUNCT_1:70;
A4: g in (dom h) /\ X by A1, RELAT_1:90;
then g in dom h by XBOOLE_0:def 4;
then r in rng h by A3, FUNCT_1:def 5;
then A5: r in dom (h " ) by FUNCT_1:55;
( g in dom h & g in X ) by A4, XBOOLE_0:def 4;
then r in h .: X by A3, FUNCT_1:def 12;
then r in (dom (h " )) /\ (h .: X) by A5, XBOOLE_0:def 4;
hence r in dom ((h " ) | (h .: X)) by RELAT_1:90; :: thesis: verum

end;

assume r in dom ((h " ) | (h .: X)) ; :: thesis: r in dom ((h | X) " )
then r in (dom (h " )) /\ (h .: X) by RELAT_1:90;
then r in h .: X by XBOOLE_0:def 4;
then consider t being set such that
A6: t in dom h and
A7: t in X and
A8: h . t = r by FUNCT_1:def 12;
t in (dom h) /\ X by A6, A7, XBOOLE_0:def 4;
then A9: t in dom (h | X) by RELAT_1:90;
(h | X) . t = r by A7, A8, FUNCT_1:72;
then r in rng hX by A9, FUNCT_1:def 5;
hence r in dom ((h | X) " ) by FUNCT_1:55; :: thesis: verum

end;

then A10: dom (hX " ) = dom ((h " ) | (h .: X)) by TARSKI:2;

now

given r being set such that A11: r in dom ((h | X) " ) and
A12: ((h | X) " ) . r <> ((h " ) | (h .: X)) . r ; :: thesis: contradiction
r in (dom (h " )) /\ (h .: X) by A10, A11, RELAT_1:90;
then r in h .: X by XBOOLE_0:def 4;
then consider t being set such that
t in dom h and
t in X and
A13: h . t = r by FUNCT_1:def 12;
r in rng hX by A11, FUNCT_1:55;
then consider g being set such that
A14: g in dom (h | X) and
A15: (h | X) . g = r by FUNCT_1:def 5;
A16: h . g = r by A14, A15, FUNCT_1:70;
g in (dom h) /\ X by A14, RELAT_1:90;
then A17: g in dom h by XBOOLE_0:def 4;
(hX " ) . r <> (h " ) . r by A10, A11, A12, FUNCT_1:70;
then g <> (h " ) . (h . t) by A14, A15, A13, FUNCT_1:56;
hence contradiction by A13, A17, A16, FUNCT_1:56; :: thesis: verum

end;

hence (h | X) " = (h " ) | (h .: X) by A10, FUNCT_1:9; :: thesis: verum