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 A3, XBOOLE_0:def 4;
then (A ") . y in dom (C | (dom A)) by RELAT_1:61;
then A . ((A ") . y) in dom D by A1, FUNCT_1:11;
then y in dom D by A2, A3, FUNCT_1:35;
then y in (dom D) /\ (dom (A ")) by A3, XBOOLE_0:def 4;
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 A2, A4, FUNCT_1:35;
then (A ") . y in dom (D * A) by A2, A5, FUNCT_1:11;
then (A ") . y in (dom C) /\ (dom A) by A1, RELAT_1:61;
then (A ") . y in dom C by XBOOLE_0:def 4;
hence y in dom (C * (A ")) by A4, FUNCT_1:11; :: 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 A7, FUNCT_1:12
.= (C | (dom A)) . ((A ") . y) by A2, A9, FUNCT_1:49
.= D . (A . ((A ") . y)) by A1, A2, A9, FUNCT_1:13
.= D . y by A2, A8, FUNCT_1:35
.= (D | (dom (A "))) . y by A8, FUNCT_1:49 ; :: thesis: verum
end;
hence C * (A ") = D | (dom (A ")) by A6, FUNCT_1:2; :: thesis: verum