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

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

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