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 "))) )

for y being object st y in dom (C * (A ")) holds

(C * (A ")) . y = (D | (dom (A "))) . y

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

then A6:
dom (C * (A ")) = dom (D | (dom (A ")))
by TARSKI:2;
let y be object ; :: thesis: ( y in dom (C * (A ")) iff y in dom (D | (dom (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;hereby :: thesis: ( y in dom (D | (dom (A "))) implies y in dom (C * (A ")) )

assume
y in dom (D | (dom (A ")))
; :: thesis: 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;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

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

for y being object st y in dom (C * (A ")) holds

(C * (A ")) . y = (D | (dom (A "))) . y

proof

hence
C * (A ") = D | (dom (A "))
by A6, FUNCT_1:2; :: thesis: verum
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;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