let A, B be set ; :: thesis: for x being object holds (A --> x) | B = (A /\ B) --> x
let x be object ; :: 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:61
.= A /\ B by A1, RELAT_1:160
.= dom ((A /\ B) --> x) by A2, RELAT_1:160 ;

now :: thesis: for z being object st z in dom ((A /\ B) --> x) holds
((A --> x) | B) . z = ((A /\ B) --> x) . z

let z be object ; :: 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:160;
then A6: z in A by XBOOLE_0:def 4;
thus ((A --> x) | B) . z = (A --> x) . z by A3, A4, FUNCT_1:47
.= x by A6, Th7
.= ((A /\ B) --> x) . z by A5, Th7 ; :: thesis: verum

end;

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