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} )

( 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} )

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