let A, B, C, D be Function; ( D * A = C | (dom A) implies (D | (dom B)) * A = C | (dom (B * A)) )
assume A1:
D * A = C | (dom A)
; (D | (dom B)) * A = C | (dom (B * A))
set f = (D | (dom B)) * A;
set g = C | (dom (B * A));
A2: dom ((D | (dom B)) * A) =
A " (dom (D | (dom B)))
by RELAT_1:147
.=
A " ((dom D) /\ (dom B))
by RELAT_1:61
.=
(A " (dom D)) /\ (A " (dom B))
by FUNCT_1:68
.=
(dom (D * A)) /\ (A " (dom B))
by RELAT_1:147
.=
(dom (C | (dom A))) /\ (dom (B * A))
by A1, RELAT_1:147
.=
((dom C) /\ (dom A)) /\ (dom (B * A))
by RELAT_1:61
.=
(dom C) /\ ((dom A) /\ (dom (B * A)))
by XBOOLE_1:16
.=
(dom C) /\ (dom (B * A))
by RELAT_1:25, XBOOLE_1:28
.=
dom (C | (dom (B * A)))
by RELAT_1:61
;
for x being object st x in dom ((D | (dom B)) * A) holds
((D | (dom B)) * A) . x = (C | (dom (B * A))) . x
hence
(D | (dom B)) * A = C | (dom (B * A))
by A2, FUNCT_1:2; verum