let A be set ; :: thesis: for x being object holds
( dom (A --> x) = A & rng (A --> x) c= {x} )
let x be object ; :: thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} )

now :: thesis: ( dom (A --> x) = A & rng (A --> x) c= {x} )

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

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

thus ( dom (A --> x) = A & rng (A --> x) c= {x} ) by A1; :: 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