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 :: thesis: for r being object holds
( ( r in dom ((h | X) ") implies r in dom ((h ") | (h .: X)) ) & ( r in dom ((h ") | (h .: X)) implies r in dom ((h | X) ") ) )
let r be object ; :: 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:33;
then consider g being object such that
A1: g in dom (h | X) and
A2: (h | X) . g = r by FUNCT_1:def 3;
A3: h . g = r by A1, A2, FUNCT_1:47;
A4: g in (dom h) /\ X by A1, RELAT_1:61;
then g in dom h by XBOOLE_0:def 4;
then r in rng h by A3, FUNCT_1:def 3;
then A5: r in dom (h ") by FUNCT_1:33;
( g in dom h & g in X ) by A4, XBOOLE_0:def 4;
then r in h .: X by A3, FUNCT_1:def 6;
then r in (dom (h ")) /\ (h .: X) by A5, XBOOLE_0:def 4;
hence r in dom ((h ") | (h .: X)) by RELAT_1:61; :: 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:61;
then r in h .: X by XBOOLE_0:def 4;
then consider t being object such that
A6: t in dom h and
A7: t in X and
A8: h . t = r by FUNCT_1:def 6;
t in (dom h) /\ X by A6, A7, XBOOLE_0:def 4;
then A9: t in dom (h | X) by RELAT_1:61;
(h | X) . t = r by A7, A8, FUNCT_1:49;
then r in rng hX by A9, FUNCT_1:def 3;
hence r in dom ((h | X) ") by FUNCT_1:33; :: thesis: verum
end;
then A10: dom (hX ") = dom ((h ") | (h .: X)) by TARSKI:2;
now :: thesis: for r being object holds
( not r in dom ((h | X) ") or not ((h | X) ") . r <> ((h ") | (h .: X)) . r )
given r being object 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:61;
then r in h .: X by XBOOLE_0:def 4;
then consider t being object such that
t in dom h and
t in X and
A13: h . t = r by FUNCT_1:def 6;
r in rng hX by A11, FUNCT_1:33;
then consider g being object such that
A14: g in dom (h | X) and
A15: (h | X) . g = r by FUNCT_1:def 3;
A16: h . g = r by A14, A15, FUNCT_1:47;
g in (dom h) /\ X by A14, RELAT_1:61;
then A17: g in dom h by XBOOLE_0:def 4;
(hX ") . r <> (h ") . r by A10, A11, A12, FUNCT_1:47;
then g <> (h ") . (h . t) by A14, A15, A13, FUNCT_1:34;
hence contradiction by A13, A17, A16, FUNCT_1:34; :: thesis: verum
end;
hence (h | X) " = (h ") | (h .: X) by A10; :: thesis: verum