let A, x, B be set ; :: thesis: (A --> x) | B = (A /\ B) --> x
A1: ( A = {} or A <> {} ) ;
A2: ( A /\ B = {} or A /\ B <> {} ) ;
A3: dom ((A --> x) | B) = (dom (A --> x)) /\ B by RELAT_1:90
.= A /\ B by A1, RELAT_1:195
.= dom ((A /\ B) --> x) by A2, RELAT_1:195 ;

now

let z be set ; :: thesis: ( z in dom ((A /\ B) --> x) implies ((A --> x) | B) . z = ((A /\ B) --> x) . z )
assume A4: z in dom ((A /\ B) --> x) ; :: thesis: ((A --> x) | B) . z = ((A /\ B) --> x) . z
( A /\ B = {} or A /\ B <> {} ) ;
then A5: z in A /\ B by A4, RELAT_1:195;
then A6: z in A by XBOOLE_0:def 4;
thus ((A --> x) | B) . z = (A --> x) . z by A3, A4, FUNCT_1:70
.= x by A6, Th13
.= ((A /\ B) --> x) . z by A5, Th13 ; :: thesis: verum

end;

hence (A --> x) | B = (A /\ B) --> x by A3, FUNCT_1:9; :: thesis: verum