let A be one-to-one Function; :: thesis: for C, D being Function st D * A = C | (dom A) holds
C * (A ") = D | (dom (A "))

let C, D be Function; :: thesis: ( D * A = C | (dom A) implies C * (A ") = D | (dom (A ")) )
assume A1: D * A = C | (dom A) ; :: thesis: C * (A ") = D | (dom (A "))
A2: ( dom A = rng (A ") & rng A = dom (A ") ) by FUNCT_1:33;
for y being object holds
( y in dom (C * (A ")) iff y in dom (D | (dom (A "))) )
proof
let y be object ; :: thesis: ( y in dom (C * (A ")) iff y in dom (D | (dom (A "))) )
hereby :: thesis: ( y in dom (D | (dom (A "))) implies y in dom (C * (A ")) )
assume y in dom (C * (A ")) ; :: thesis: y in dom (D | (dom (A ")))
then A3: ( y in dom (A ") & (A ") . y in dom C ) by FUNCT_1:11;
then (A ") . y in rng (A ") by FUNCT_1:3;
then (A ") . y in dom A by FUNCT_1:33;
then (A ") . y in (dom C) /\ (dom A) by ;
then (A ") . y in dom (C | (dom A)) by RELAT_1:61;
then A . ((A ") . y) in dom D by ;
then y in dom D by ;
then y in (dom D) /\ (dom (A ")) by ;
hence y in dom (D | (dom (A "))) by RELAT_1:61; :: thesis: verum
end;
assume y in dom (D | (dom (A "))) ; :: thesis: y in dom (C * (A "))
then y in (dom D) /\ (dom (A ")) by RELAT_1:61;
then A4: ( y in dom D & y in dom (A ") ) by XBOOLE_0:def 4;
then A5: (A ") . y in rng (A ") by FUNCT_1:3;
A . ((A ") . y) in dom D by ;
then (A ") . y in dom (D * A) by ;
then (A ") . y in (dom C) /\ (dom A) by ;
then (A ") . y in dom C by XBOOLE_0:def 4;
hence y in dom (C * (A ")) by ; :: thesis: verum
end;
then A6: dom (C * (A ")) = dom (D | (dom (A "))) by TARSKI:2;
for y being object st y in dom (C * (A ")) holds
(C * (A ")) . y = (D | (dom (A "))) . y
proof
let y be object ; :: thesis: ( y in dom (C * (A ")) implies (C * (A ")) . y = (D | (dom (A "))) . y )
assume A7: y in dom (C * (A ")) ; :: thesis: (C * (A ")) . y = (D | (dom (A "))) . y
then A8: ( y in dom (A ") & (A ") . y in dom C ) by FUNCT_1:11;
then A9: (A ") . y in rng (A ") by FUNCT_1:3;
thus (C * (A ")) . y = C . ((A ") . y) by
.= (C | (dom A)) . ((A ") . y) by
.= D . (A . ((A ") . y)) by
.= D . y by
.= (D | (dom (A "))) . y by ; :: thesis: verum
end;
hence C * (A ") = D | (dom (A ")) by ; :: thesis: verum