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) & (h | X) . g = r ) by FUNCT_1:def 5;
( g in (dom h) /\ X & h . g = r ) by A1, FUNCT_1:68;
then ( g in dom h & g in X & h . g = r ) by XBOOLE_0:def 4;
then ( r in rng h & g in dom h & g in X & h . g = r ) by FUNCT_1:def 5;
then ( r in dom (h " ) & r in h .: X ) by FUNCT_1:55, FUNCT_1:def 12;
then r in (dom (h " )) /\ (h .: X) by 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
A2: ( t in dom h & t in X & h . t = r ) by FUNCT_1:def 12;
( t in (dom h) /\ X & (h | X) . t = r ) by A2, FUNCT_1:72, XBOOLE_0:def 4;
then ( t in dom (h | X) & (h | X) . t = r ) by RELAT_1:90;
then r in rng hX by FUNCT_1:def 5;
hence r in dom ((h | X) " ) by FUNCT_1:55; :: thesis: verum

end;

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

now

given r being set such that A4: r in dom ((h | X) " ) and
A5: ((h | X) " ) . r <> ((h " ) | (h .: X)) . r ; :: thesis: contradiction
A6: (hX " ) . r <> (h " ) . r by A3, A4, A5, FUNCT_1:68;
r in rng hX by A4, FUNCT_1:55;
then consider g being set such that
A7: ( g in dom (h | X) & (h | X) . g = r ) by FUNCT_1:def 5;
r in (dom (h " )) /\ (h .: X) by A3, A4, RELAT_1:90;
then r in h .: X by XBOOLE_0:def 4;
then consider t being set such that
A8: ( t in dom h & t in X & h . t = r ) by FUNCT_1:def 12;
A9: g <> (h " ) . (h . t) by A6, A7, A8, FUNCT_1:56;
( g in (dom h) /\ X & h . g = r ) by A7, FUNCT_1:68;
then ( g in dom h & h . g = r ) by XBOOLE_0:def 4;
hence contradiction by A8, A9, FUNCT_1:56; :: thesis: verum

end;

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