let A, x, B be set ; :: thesis: ( x in B implies (A --> x) " B = A )
assume A1: x in B ; :: thesis: (A --> x) " B = A

now

per cases ( A = {} or A <> {} ) ;

suppose A2: A = {} ; :: thesis: (A --> x) " B = A

rng ({} --> x) = {} ;
then (rng (A --> x)) /\ B = {} by A2;
then rng (A --> x) misses B by XBOOLE_0:def 7;
hence (A --> x) " B = A by A2, RELAT_1:173; :: thesis: verum

end;

suppose A <> {} ; :: thesis: (A --> x) " B = A

then A3: rng (A --> x) = {x} by RELAT_1:195;
{x} c= B by A1, ZFMISC_1:37;
then {x} /\ B = {x} by XBOOLE_1:28;
hence (A --> x) " B = (A --> x) " {x} by A3, RELAT_1:168
.= dom (A --> x) by A3, RELAT_1:169
.= A by Th19 ;
:: thesis: verum

end;

end;

end;

hence (A --> x) " B = A ; :: thesis: verum