let A, B, C, D be Function; :: thesis: ( D * A = C | (dom A) implies (D | (dom B)) * A = C | (dom (B * A)) )
assume A1: D * A = C | (dom A) ; :: thesis: (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

proof

let x be object ; :: thesis: ( x in dom ((D | (dom B)) * A) implies ((D | (dom B)) * A) . x = (C | (dom (B * A))) . x )
assume A3: x in dom ((D | (dom B)) * A) ; :: thesis: ((D | (dom B)) * A) . x = (C | (dom (B * A))) . x
then A4: ( x in dom A & A . x in dom (D | (dom B)) ) by FUNCT_1:11;
A5: x in dom (C | (dom (B * A))) by A2, A3;
thus ((D | (dom B)) * A) . x = (D | (dom B)) . (A . x) by A3, FUNCT_1:12
.= D . (A . x) by A4, FUNCT_1:47
.= (D * A) . x by A4, FUNCT_1:13
.= C . x by A4, A1, FUNCT_1:49
.= (C | (dom (B * A))) . x by A5, FUNCT_1:47 ; :: thesis: verum

end;

hence (D | (dom B)) * A = C | (dom (B * A)) by A2, FUNCT_1:2; :: thesis: verum