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

now :: thesis: (A --> x) " B = A

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

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

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

end;

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

then A3: rng (A --> x) = {x} by RELAT_1:160;
{x} c= B by A1, ZFMISC_1:31;
then {x} /\ B = {x} by XBOOLE_1:28;
hence (A --> x) " B = (A --> x) " {x} by A3, RELAT_1:133
.= dom (A --> x) by A3, RELAT_1:134
.= A ;
:: thesis: verum

end;

end;

end;

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