let A, x be set ; :: thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} )

now

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

suppose A1: A = {} ; :: thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} )

rng ({} --> x) = {} ;
hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) by A1, XBOOLE_1:2; :: thesis: verum

end;

suppose A <> {} ; :: thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} )

hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) by RELAT_1:160; :: thesis: verum

end;

end;

end;

hence ( dom (A --> x) = A & rng (A --> x) c= {x} ) ; :: thesis: verum